Addition

Analysis I, Section 2.2: Addition

This file is a translation of Section 2.2 of Analysis I to Lean 4. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of addition and order for the "Chapter 2" natural numbers, Chapter2.Nat : TypeChapter2.Nat.
Establishment of basic properties of addition and order.

Note: at the end of this chapter, the Chapter2.Nat : TypeChapter2.Nat class will be deprecated in favor of the standard Mathlib class Nat : Type_root_.Nat, or ℕ : Typeℕ. However, we will develop the properties of Chapter2.Nat : TypeChapter2.Nat "by hand" for pedagogical purposes.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter2

Definition 2.2.1. (Addition of natural numbers). Compare with Mathlib's Chapter2.Nat.add (n m : Nat) : NatNat.add

abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n

This instance allows for the notation to be used for natural number addition.

instance Nat.instAdd : Add Nat where
  add := add

Compare with Mathlib's Chapter2.Nat.zero_add (m : Nat) : 0 + m = mNat.zero_add.

@[simp]
theorem Nat.zero_add (m: Nat) : 0 + m = m := recurse_zero (fun _ sum ↦ sum++) _

Compare with Mathlib's Chapter2.Nat.succ_add (n m : Nat) : n++ + m = (n + m)++Nat.succ_add.

theorem Nat.succ_add (n m: Nat) : n++ + m = (n+m)++ := byn:Natm:Nat⊢ n++ + m = (n + m)++ rflAll goals completed! 🐙

Compare with Mathlib's Chapter2.Nat.one_add (m : Nat) : 1 + m = m++Nat.one_add.

theorem Nat.one_add (m:Nat) : 1 + m = m++ := bym:Nat⊢ 1 + m = m++
  rw [show 1 = 0++ from rfl, succ_add, zero_add]All goals completed! 🐙

theorem Nat.two_add (m:Nat) : 2 + m = (m++)++ := bym:Nat⊢ 2 + m = m++++
  rw [show 2 = 1++ from rfl, succ_add, one_add]All goals completed! 🐙

example : (2:Nat) + 3 = 5 := by⊢ 2 + 3 = 5
  rw [Nat.two_add, show 3++=4 from rfl, show 4++=5 from rfl]All goals completed! 🐙

fun n m => n + m : Nat → Nat → Nat

Lemma 2.2.2 (n + 0 = n). Compare with Mathlib's Chapter2.Nat.add_zero (n : Nat) : n + 0 = nNat.add_zero.

@[simp]
lemma Nat.add_zero (n:Nat) : n + 0 = n := byn:Nat⊢ n + 0 = n
  -- This proof is written to follow the structure of the original text.
  revert n⊢ ∀ (n : Nat), n + 0 = n; apply inductionhbase⊢ 0 + 0 = 0hind⊢ ∀ (n : Nat), n + 0 = n → n++ + 0 = n++
  .hbase⊢ 0 + 0 = 0 exact zero_add 0All goals completed! 🐙
  intro n ihhindn:Natih:n + 0 = n⊢ n++ + 0 = n++
  calc
    (n++) + 0 = (n + 0)++ := byn:Natih:n + 0 = n⊢ n++ + 0 = (n + 0)++ rflAll goals completed! 🐙
    _ = n++ := byn:Natih:n + 0 = n⊢ (n + 0)++ = n++ rw [ih]All goals completed! 🐙

Lemma 2.2.3 (n+(m++) = (n+m)++). Compare with Mathlib's Chapter2.Nat.add_succ (n m : Nat) : n + m++ = (n + m)++Nat.add_succ.

lemma Nat.add_succ (n m:Nat) : n + (m++) = (n + m)++ := byn:Natm:Nat⊢ n + m++ = (n + m)++
  -- this proof is written to follow the structure of the original text.
  revert nm:Nat⊢ ∀ (n : Nat), n + m++ = (n + m)++; apply inductionhbasem:Nat⊢ 0 + m++ = (0 + m)++hindm:Nat⊢ ∀ (n : Nat), n + m++ = (n + m)++ → n++ + m++ = (n++ + m)++
  .hbasem:Nat⊢ 0 + m++ = (0 + m)++ rw [zero_add, zero_add]All goals completed! 🐙
  intro n ihhindm:Natn:Natih:n + m++ = (n + m)++⊢ n++ + m++ = (n++ + m)++
  rw [succ_add, ih]hindm:Natn:Natih:n + m++ = (n + m)++⊢ (n + m)++++ = (n++ + m)++
  rw [succ_add]All goals completed! 🐙

n++ = n + 1 (Why?). Compare with Mathlib's Chapter2.Nat.succ_eq_add_one (n : Nat) : n++ = n + 1Nat.succ_eq_add_one

theorem declaration uses 'sorry'Nat.succ_eq_add_one (n:Nat) : n++ = n + 1 := byn:Nat⊢ n++ = n + 1
  sorryAll goals completed! 🐙

Proposition 2.2.4 (Addition is commutative). Compare with Mathlib's Chapter2.Nat.add_comm (n m : Nat) : n + m = m + nNat.add_comm

theorem Nat.add_comm (n m:Nat) : n + m = m + n := byn:Natm:Nat⊢ n + m = m + n
  -- this proof is written to follow the structure of the original text.
  revert nm:Nat⊢ ∀ (n : Nat), n + m = m + n; apply inductionhbasem:Nat⊢ 0 + m = m + 0hindm:Nat⊢ ∀ (n : Nat), n + m = m + n → n++ + m = m + n++
  .hbasem:Nat⊢ 0 + m = m + 0 rw [zero_add, add_zero]All goals completed! 🐙
  intro n ihhindm:Natn:Natih:n + m = m + n⊢ n++ + m = m + n++
  rw [succ_add]hindm:Natn:Natih:n + m = m + n⊢ (n + m)++ = m + n++
  rw [add_succ, ih]All goals completed! 🐙

Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1 Compare with Mathlib's Chapter2.Nat.add_assoc (a b c : Nat) : a + b + c = a + (b + c)Nat.add_assoc.

theorem declaration uses 'sorry'Nat.add_assoc (a b c:Nat) : (a + b) + c = a + (b + c) := bya:Natb:Natc:Nat⊢ a + b + c = a + (b + c)
  sorryAll goals completed! 🐙

Proposition 2.2.6 (Cancellation law). Compare with Mathlib's Chapter2.Nat.add_left_cancel (a b c : Nat) (habc : a + b = a + c) : b = cNat.add_left_cancel.

theorem Nat.add_left_cancel (a b c:Nat) (habc: a + b = a + c) : b = c := bya:Natb:Natc:Nathabc:a + b = a + c⊢ b = c
  -- This proof is written to follow the structure of the original text.
  revert ab:Natc:Nat⊢ ∀ (a : Nat), a + b = a + c → b = c; apply inductionhbaseb:Natc:Nat⊢ 0 + b = 0 + c → b = chindb:Natc:Nat⊢ ∀ (n : Nat), (n + b = n + c → b = c) → n++ + b = n++ + c → b = c
  .hbaseb:Natc:Nat⊢ 0 + b = 0 + c → b = c intro hbchbaseb:Natc:Nathbc:0 + b = 0 + c⊢ b = c
    rwa [zero_add, zero_add]hbaseb:Natc:Nathbc:b = c⊢ b = c at hbc
  intro a ihhindb:Natc:Nata:Natih:a + b = a + c → b = c⊢ a++ + b = a++ + c → b = c
  intro hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:a++ + b = a++ + c⊢ b = c
  rw [succ_add, succ_add] at hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:(a + b)++ = (a + c)++⊢ b = c
  replace hbc := succ_cancel hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:?_mvar.2309 := Chapter2.Nat.succ_cancel _fvar.2300⊢ b = c
  exact ih hbcAll goals completed! 🐙

(Not from textbook) Nat can be given the structure of a commutative additive monoid. This permits tactics such as Unknown identifier `abel`abel to apply to the Chapter 2 natural numbers.

instance Nat.addCommMonoid : AddCommMonoid Nat where
  add_assoc := add_assoc
  add_comm := add_comm
  zero_add := zero_add
  add_zero := add_zero
  nsmul := nsmulRec

This illustration of the Unknown identifier `abel`abel tactic is not from the textbook.

example (a b c d:Nat) : (a+b)+(c+0+d) = (b+c)+(d+a) := bya:Natb:Natc:Natd:Nat⊢ a + b + (c + 0 + d) = b + c + (d + a) abelAll goals completed! 🐙

Definition 2.2.7 (Positive natural numbers).

def Nat.IsPos (n:Nat) : Prop := n ≠ 0

theorem Nat.isPos_iff (n:Nat) : n.IsPos ↔ n ≠ 0 := byn:Nat⊢ n.IsPos ↔ n ≠ 0 rflAll goals completed! 🐙

Proposition 2.2.8 (positive plus natural number is positive). Compare with Mathlib's Chapter2.Nat.add_pos_left {a : Nat} (b : Nat) (ha : a.IsPos) : (a + b).IsPosNat.add_pos_left.

theorem Nat.add_pos_left {a:Nat} (b:Nat) (ha: a.IsPos) : (a + b).IsPos := bya:Natb:Natha:a.IsPos⊢ (a + b).IsPos
  -- This proof is written to follow the structure of the original text.
  revert ba:Natha:a.IsPos⊢ ∀ (b : Nat), (a + b).IsPos; apply inductionhbasea:Natha:a.IsPos⊢ (a + 0).IsPoshinda:Natha:a.IsPos⊢ ∀ (n : Nat), (a + n).IsPos → (a + n++).IsPos
  .hbasea:Natha:a.IsPos⊢ (a + 0).IsPos rwa [add_zero]hbasea:Natha:a.IsPos⊢ a.IsPos
  intro b habhinda:Natha:a.IsPosb:Nathab:(a + b).IsPos⊢ (a + b++).IsPos
  rw [add_succ]hinda:Natha:a.IsPosb:Nathab:(a + b).IsPos⊢ (a + b)++.IsPos
  have : (a+b)++ ≠ 0 := succ_ne _hinda:Natha:a.IsPosb:Nathab:(a + b).IsPosthis:(_fvar.4023 + _fvar.4071)++ ≠ 0 := Chapter2.Nat.succ_ne ?_mvar.4176⊢ (a + b)++.IsPos
  exact thisAll goals completed! 🐙

Compare with Mathlib's Chapter2.Nat.add_pos_right {a : Nat} (b : Nat) (ha : a.IsPos) : (b + a).IsPosNat.add_pos_right.

This theorem is a consequence of the previous theorem and add_comm.{u_1} {G : Type u_1} [AddCommMagma G] (a b : G) : a + b = b + aadd_comm, and Unknown identifier `grind`grind can automatically discover such proofs.

theorem Nat.add_pos_right {a:Nat} (b:Nat) (ha: a.IsPos) : (b + a).IsPos := bya:Natb:Natha:a.IsPos⊢ (b + a).IsPos
  grind [add_comm, add_pos_left]All goals completed! 🐙

Corollary 2.2.9 (if sum vanishes, then summands vanish). Compare with Mathlib's Chapter2.Nat.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 0Nat.add_eq_zero.

theorem Nat.add_eq_zero (a b:Nat) (hab: a + b = 0) : a = 0 ∧ b = 0 := bya:Natb:Nathab:a + b = 0⊢ a = 0 ∧ b = 0
  -- This proof is written to follow the structure of the original text.
  by_contra ha:Natb:Nathab:a + b = 0h:¬(a = 0 ∧ b = 0)⊢ False
  simp only [not_and_or, ←ne_eq] at ha:Natb:Nathab:a + b = 0h:a ≠ 0 ∨ b ≠ 0⊢ False
  obtain ha | hb := hinla:Natb:Nathab:a + b = 0ha:a ≠ 0⊢ Falseinra:Natb:Nathab:a + b = 0hb:b ≠ 0⊢ False
  .inla:Natb:Nathab:a + b = 0ha:a ≠ 0⊢ False rw [← isPos_iff] at hainla:Natb:Nathab:a + b = 0ha:a.IsPos⊢ False
    observe : (a + b).IsPosinla:Natb:Nathab:a + b = 0ha:a.IsPosthis:(a + b).IsPos⊢ False
    contradictionAll goals completed! 🐙
  rw [← isPos_iff] at hbinra:Natb:Nathab:a + b = 0hb:b.IsPos⊢ False
  observe : (a + b).IsPosinra:Natb:Nathab:a + b = 0hb:b.IsPosthis:(a + b).IsPos⊢ False
  contradictionAll goals completed! 🐙

existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)
  (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x

Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2

lemma declaration uses 'sorry'Nat.uniq_succ_eq (a:Nat) (ha: a.IsPos) : ∃! b, b++ = a := bya:Natha:a.IsPos⊢ ∃! b, b++ = a
  sorryAll goals completed! 🐙

Definition 2.2.11 (Ordering of the natural numbers). This defines the notation on the natural numbers.

instance Nat.instLE : LE Nat where
  le n m := ∃ a:Nat, m = n + a

Definition 2.2.11 (Ordering of the natural numbers). This defines the notation on the natural numbers.

instance Nat.instLT : LT Nat where
  lt n m := n ≤ m ∧ n ≠ m

lemma Nat.le_iff (n m:Nat) : n ≤ m ↔ ∃ a:Nat, m = n + a := byn:Natm:Nat⊢ n ≤ m ↔ ∃ a, m = n + a rflAll goals completed! 🐙

lemma Nat.lt_iff (n m:Nat) : n < m ↔ (∃ a:Nat, m = n + a) ∧ n ≠ m := byn:Natm:Nat⊢ n < m ↔ (∃ a, m = n + a) ∧ n ≠ m rflAll goals completed! 🐙

Compare with Mathlib's ge_iff_le.{u_1} {α : Type u_1} [LE α] {x y : α} : x ≥ y ↔ y ≤ xge_iff_le.

@[symm]
lemma Nat.ge_iff_le (n m:Nat) : n ≥ m ↔ m ≤ n := byn:Natm:Nat⊢ n ≥ m ↔ m ≤ n rflAll goals completed! 🐙

Compare with Mathlib's gt_iff_lt.{u_1} {α : Type u_1} [LT α] {x y : α} : x > y ↔ y < xgt_iff_lt.

@[symm]
lemma Nat.gt_iff_lt (n m:Nat) : n > m ↔ m < n := byn:Natm:Nat⊢ n > m ↔ m < n rflAll goals completed! 🐙

Compare with Mathlib's Chapter2.Nat.le_of_lt {n m : Nat} (hnm : n < m) : n ≤ mNat.le_of_lt.

lemma Nat.le_of_lt {n m:Nat} (hnm: n < m) : n ≤ m := hnm.1

Compare with Mathlib's Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : n ≤ m ↔ n < m ∨ n = mNat.le_iff_lt_or_eq.

lemma Nat.le_iff_lt_or_eq (n m:Nat) : n ≤ m ↔ n < m ∨ n = m := byn:Natm:Nat⊢ n ≤ m ↔ n < m ∨ n = m
  rw [Nat.le_iff, Nat.lt_iff]n:Natm:Nat⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m
  by_cases h : n = mpos._@._hyg.1628n:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = mneg._@._hyg.1628n:Natm:Nath:¬n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m
  .pos._@._hyg.1628n:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m simp [h]pos._@._hyg.1628n:Natm:Nath:n = m⊢ ∃ a, m = m + a
    use 0hn:Natm:Nath:n = m⊢ m = m + 0
    rw [add_zero]All goals completed! 🐙
  simp [h]All goals completed! 🐙

example : (8:Nat) > 5 := by⊢ 8 > 5
  rw [Nat.gt_iff_lt, Nat.lt_iff]⊢ (∃ a, 8 = 5 + a) ∧ 5 ≠ 8
  constructorleft⊢ ∃ a, 8 = 5 + aright⊢ 5 ≠ 8
  .left⊢ ∃ a, 8 = 5 + a have : (8:Nat) = 5 + 3 := by⊢ 8 > 5 rflAll goals completed! 🐙
    rw [this]leftthis:8 = 5 + 3 := ?_mvar.63377⊢ ∃ a, 5 + 3 = 5 + a
    use 3All goals completed! 🐙
  decideAll goals completed! 🐙

Compare with Mathlib's Nat.lt_succ_self (n : ℕ) : n < n.succNat.lt_succ_self.

theorem declaration uses 'sorry'Nat.succ_gt_self (n:Nat) : n++ > n := byn:Nat⊢ n++ > n
  sorryAll goals completed! 🐙

Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3

(a) (Order is reflexive). Compare with Mathlib's Chapter2.Nat.le_refl (a : Nat) : a ≤ aNat.le_refl.

theorem declaration uses 'sorry'Nat.ge_refl (a:Nat) : a ≥ a := bya:Nat⊢ a ≥ a
  sorryAll goals completed! 🐙

@[refl]
theorem Nat.le_refl (a:Nat) : a ≤ a := a.ge_refl

The refl tag allows for the rfl.{u} {α : Sort u} {a : α} : a = arfl tactic to work for inequalities.

example (a b:Nat): a+b ≥ a+b := bya:Natb:Nat⊢ a + b ≥ a + b rflAll goals completed! 🐙

(b) (Order is transitive). The Unknown identifier `obtain`obtain tactic will be useful here. Compare with Mathlib's Chapter2.Nat.le_trans {a b c : Nat} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ cNat.le_trans.

theorem declaration uses 'sorry'Nat.ge_trans {a b c:Nat} (hab: a ≥ b) (hbc: b ≥ c) : a ≥ c := bya:Natb:Natc:Nathab:a ≥ bhbc:b ≥ c⊢ a ≥ c
  sorryAll goals completed! 🐙

theorem Nat.le_trans {a b c:Nat} (hab: a ≤ b) (hbc: b ≤ c) : a ≤ c := Nat.ge_trans hbc hab

(c) (Order is anti-symmetric). Compare with Mathlib's Nat.le_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m ≤ n) : n = mNat.le_antisymm.

theorem declaration uses 'sorry'Nat.ge_antisymm {a b:Nat} (hab: a ≥ b) (hba: b ≥ a) : a = b := bya:Natb:Nathab:a ≥ bhba:b ≥ a⊢ a = b
  sorryAll goals completed! 🐙

(d) (Addition preserves order). Compare with Mathlib's Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + cNat.add_le_add_right.

theorem declaration uses 'sorry'Nat.add_ge_add_right (a b c:Nat) : a ≥ b ↔ a + c ≥ b + c := bya:Natb:Natc:Nat⊢ a ≥ b ↔ a + c ≥ b + c
  sorryAll goals completed! 🐙

(d) (Addition preserves order). Compare with Mathlib's Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + bNat.add_le_add_left.

theorem Nat.add_ge_add_left (a b c:Nat) : a ≥ b ↔ c + a ≥ c + b := bya:Natb:Natc:Nat⊢ a ≥ b ↔ c + a ≥ c + b
  simp only [add_comm]a:Natb:Natc:Nat⊢ a ≥ b ↔ a + c ≥ b + c
  exact add_ge_add_right _ _ _All goals completed! 🐙

(d) (Addition preserves order). Compare with Mathlib's Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + cNat.add_le_add_right.

theorem Nat.add_le_add_right (a b c:Nat) : a ≤ b ↔ a + c ≤ b + c := add_ge_add_right _ _ _

(d) (Addition preserves order). Compare with Mathlib's Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + bNat.add_le_add_left.

theorem Nat.add_le_add_left (a b c:Nat) : a ≤ b ↔ c + a ≤ c + b := add_ge_add_left _ _ _

(e) a < b iff a++ ≤ b. Compare with Mathlib's Nat.succ_le_iff {m n : ℕ} : m.succ ≤ n ↔ m < nNat.succ_le_iff.

theorem declaration uses 'sorry'Nat.lt_iff_succ_le (a b:Nat) : a < b ↔ a++ ≤ b := bya:Natb:Nat⊢ a < b ↔ a++ ≤ b
  sorryAll goals completed! 🐙

(f) a < b if and only if b = a + d for positive d.

theorem declaration uses 'sorry'Nat.lt_iff_add_pos (a b:Nat) : a < b ↔ ∃ d:Nat, d.IsPos ∧ b = a + d := bya:Natb:Nat⊢ a < b ↔ ∃ d, d.IsPos ∧ b = a + d
  sorryAll goals completed! 🐙

If a < b then a ̸= b,

theorem Nat.ne_of_lt (a b:Nat) : a < b → a ≠ b := bya:Natb:Nat⊢ a < b → a ≠ b
  intro ha:Natb:Nath:a < b⊢ a ≠ b; exact h.2All goals completed! 🐙

if a > b then a ̸= b.

theorem Nat.ne_of_gt (a b:Nat) : a > b → a ≠ b := bya:Natb:Nat⊢ a > b → a ≠ b
  intro ha:Natb:Nath:a > b⊢ a ≠ b; exact h.2.symmAll goals completed! 🐙

If a > b and a < b then contradiction

theorem Nat.not_lt_of_gt (a b:Nat) : a < b ∧ a > b → False := bya:Natb:Nat⊢ a < b ∧ a > b → False
  intro ha:Natb:Nath:a < b ∧ a > b⊢ False
  have := (ge_antisymm (le_of_lt h.1) (le_of_lt h.2)).symma:Natb:Nath:a < b ∧ a > bthis:?_mvar.64965 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False
  have := ne_of_lt _ _ h.1a:Natb:Nath:a < b ∧ a > bthis✝:?_mvar.64965 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:?_mvar.65002 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False
  contradictionAll goals completed! 🐙

theorem Nat.not_lt_self {a: Nat} (h : a < a) : False := bya:Nath:a < a⊢ False
  apply not_lt_of_gt a aa:Nath:a < a⊢ a < a ∧ a > a
  simp [h]All goals completed! 🐙

theorem Nat.lt_of_le_of_lt {a b c : Nat} (hab: a ≤ b) (hbc: b < c) : a < c := bya:Natb:Natc:Nathab:a ≤ bhbc:b < c⊢ a < c
  rw [lt_iff_add_pos] at *a:Natb:Natc:Nathab:a ≤ bhbc:∃ d, d.IsPos ∧ c = b + d⊢ ∃ d, d.IsPos ∧ c = a + d
  choose d hd using haba:Natb:Natc:Nathbc:∃ d, d.IsPos ∧ c = b + dd:Nathd:b = a + d⊢ ∃ d, d.IsPos ∧ c = a + d
  choose e he1 he2 using hbca:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ ∃ d, d.IsPos ∧ c = a + d
  use d + eha:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPos ∧ c = a + (d + e); split_andsh.refine_1a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPosh.refine_2a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ c = a + (d + e)
  .h.refine_1a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPos exact add_pos_right d he1All goals completed! 🐙
  .h.refine_2a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ c = a + (d + e) rw [he2, hd, add_assoc]All goals completed! 🐙

This lemma was a Unknown identifier `why?`why? statement from Proposition 2.2.13, but is more broadly useful, so is extracted here.

theorem declaration uses 'sorry'Nat.zero_le (a:Nat) : 0 ≤ a := bya:Nat⊢ 0 ≤ a
  sorryAll goals completed! 🐙

Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4 Compare with Mathlib's trichotomous.{u_1} {α : Sort u_1} {r : α → α → Prop} [IsTrichotomous α r] (a b : α) : r a b ∨ a = b ∨ r b atrichotomous. Parts of this theorem have been placed in the preceding Lean theorems.

theorem declaration uses 'sorry'Nat.trichotomous (a b:Nat) : a < b ∨ a = b ∨ a > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b
  -- This proof is written to follow the structure of the original text.
  revert ab:Nat⊢ ∀ (a : Nat), a < b ∨ a = b ∨ a > b; apply inductionhbaseb:Nat⊢ 0 < b ∨ 0 = b ∨ 0 > bhindb:Nat⊢ ∀ (n : Nat), n < b ∨ n = b ∨ n > b → n++ < b ∨ n++ = b ∨ n++ > b
  .hbaseb:Nat⊢ 0 < b ∨ 0 = b ∨ 0 > b observe why : 0 ≤ bhbaseb:Natwhy:0 ≤ b⊢ 0 < b ∨ 0 = b ∨ 0 > b
    rw [le_iff_lt_or_eq] at whyhbaseb:Natwhy:0 < b ∨ 0 = b⊢ 0 < b ∨ 0 = b ∨ 0 > b
    tautoAll goals completed! 🐙
  intro a ihhindb:Nata:Natih:a < b ∨ a = b ∨ a > b⊢ a++ < b ∨ a++ = b ∨ a++ > b
  obtain case1 | case2 | case3 := ihhind.inlb:Nata:Natcase1:a < b⊢ a++ < b ∨ a++ = b ∨ a++ > bhind.inr.inlb:Nata:Natcase2:a = b⊢ a++ < b ∨ a++ = b ∨ a++ > bhind.inr.inrb:Nata:Natcase3:a > b⊢ a++ < b ∨ a++ = b ∨ a++ > b
  .hind.inlb:Nata:Natcase1:a < b⊢ a++ < b ∨ a++ = b ∨ a++ > b rw [lt_iff_succ_le] at case1hind.inlb:Nata:Natcase1:a++ ≤ b⊢ a++ < b ∨ a++ = b ∨ a++ > b
    rw [le_iff_lt_or_eq] at case1hind.inlb:Nata:Natcase1:a++ < b ∨ a++ = b⊢ a++ < b ∨ a++ = b ∨ a++ > b
    tautoAll goals completed! 🐙
  .hind.inr.inlb:Nata:Natcase2:a = b⊢ a++ < b ∨ a++ = b ∨ a++ > b have why : a++ > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b sorryAll goals completed! 🐙
    tautoAll goals completed! 🐙
  have why : a++ > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b sorryAll goals completed! 🐙
  tautoAll goals completed! 🐙

(Not from textbook) Establish the decidability of this order computably. The portion of the proof involving decidability has been provided; the remaining sorries involve claims about the natural numbers. One could also have established this result by the Unknown identifier `classical`classical tactic followed by Unknown identifier `exact`exact Classical.decRel _, but this would make this definition (as well as some instances below) noncomputable.

Compare with Mathlib's Chapter2.Nat.decLe (a b : Nat) : Decidable (a ≤ b)Nat.decLe.

def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Nat.decLe : (a b : Nat) → Decidable (a ≤ b)
  | 0, b =>b:Nat⊢ Decidable (0 ≤ b) byb:Nat⊢ Decidable (0 ≤ b)
    apply isTruehb:Nat⊢ 0 ≤ b
    sorryAll goals completed! 🐙
  | a++, b =>a:Natb:Nat⊢ Decidable (a++ ≤ b) bya:Natb:Nat⊢ Decidable (a++ ≤ b)
    cases decLe a b with
    | isTrue h =>isTruea:Natb:Nath:a ≤ b⊢ Decidable (a++ ≤ b)
      cases decEq a b with
      | isTrue h =>isTrue.isTruea:Natb:Nath✝:a ≤ bh:a = b⊢ Decidable (a++ ≤ b)
        apply isFalseisTrue.isTrue.ha:Natb:Nath✝:a ≤ bh:a = b⊢ ¬a++ ≤ b
        sorryAll goals completed! 🐙
      | isFalse h =>isTrue.isFalsea:Natb:Nath✝:a ≤ bh:¬a = b⊢ Decidable (a++ ≤ b)
        apply isTrueisTrue.isFalse.ha:Natb:Nath✝:a ≤ bh:¬a = b⊢ a++ ≤ b
        sorryAll goals completed! 🐙
    | isFalse h =>isFalsea:Natb:Nath:¬a ≤ b⊢ Decidable (a++ ≤ b)
      apply isFalseisFalse.ha:Natb:Nath:¬a ≤ b⊢ ¬a++ ≤ b
      sorryAll goals completed! 🐙

instance Nat.decidableRel : DecidableRel (·≤ ·: Nat → Nat → Prop) := Nat.decLe

(Not from textbook) Nat has the structure of a linear ordering. This allows for tactics such as Unknown identifier `order`order and to be applicable to the Chapter 2 natural numbers.

instance Nat.instLinearOrder : LinearOrder Nat where
  le_refl := ge_refl
  le_trans a b c hab hbc := ge_trans hbc hab
  lt_iff_le_not_ge a b := bya:Natb:Nat⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
    constructormpa:Natb:Nat⊢ a < b → a ≤ b ∧ ¬b ≤ ampra:Natb:Nat⊢ a ≤ b ∧ ¬b ≤ a → a < b
    .mpa:Natb:Nat⊢ a < b → a ≤ b ∧ ¬b ≤ a intro hmpa:Natb:Nath:a < b⊢ a ≤ b ∧ ¬b ≤ a; refine ⟨ le_of_lt h, ?_ ⟩mpa:Natb:Nath:a < b⊢ ¬b ≤ a
      by_contra h'mpa:Natb:Nath:a < bh':b ≤ a⊢ False
      exact not_lt_self (lt_of_le_of_lt h' h)All goals completed! 🐙
    rintro ⟨ h1, h2 ⟩mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a < b
    rw [lt_iff, ←le_iff]mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a ≤ b ∧ a ≠ b; refine ⟨ h1, ?_ ⟩mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a ≠ b
    by_contra hmpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ ah:a = b⊢ False
    subst hmpr.introa:Nath1:a ≤ ah2:¬a ≤ a⊢ False
    contradictionAll goals completed! 🐙
  le_antisymm a b hab hba := ge_antisymm hba hab
  le_total a b := bya:Natb:Nat⊢ a ≤ b ∨ b ≤ a
    obtain h | rfl | h := trichotomous a binla:Natb:Nath:a < b⊢ a ≤ b ∨ b ≤ ainr.inla:Nat⊢ a ≤ a ∨ a ≤ ainr.inra:Natb:Nath:a > b⊢ a ≤ b ∨ b ≤ a
    .inla:Natb:Nath:a < b⊢ a ≤ b ∨ b ≤ a leftinl.ha:Natb:Nath:a < b⊢ a ≤ b; exact le_of_lt hAll goals completed! 🐙
    .inr.inla:Nat⊢ a ≤ a ∨ a ≤ a simp [ge_refl]All goals completed! 🐙
    .inr.inra:Natb:Nath:a > b⊢ a ≤ b ∨ b ≤ a rightinr.inr.ha:Natb:Nath:a > b⊢ b ≤ a; exact le_of_lt hAll goals completed! 🐙
  toDecidableLE := decidableRel

This illustration of the Unknown identifier `order`order tactic is not from the textbook.

example (a b c d:Nat) (hab: a ≤ b) (hbc: b ≤ c) (hcd: c ≤ d)
        (hda: d ≤ a) : a = c := bya:Natb:Natc:Natd:Nathab:a ≤ bhbc:b ≤ chcd:c ≤ dhda:d ≤ a⊢ a = c orderAll goals completed! 🐙

An illustration of the tactic with .

example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hcd: c ≤ d)
        (hde: d ≤ e) : a + 0 < e := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chcd:c ≤ dhde:d ≤ e⊢ a + 0 < e
  calc
    a + 0 = a := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chcd:c ≤ dhde:d ≤ e⊢ a + 0 = a simpAll goals completed! 🐙
        _ ≤ b := hab
        _ < c := hbc
        _ ≤ d := hcd
        _ ≤ e := hde

(Not from textbook) Nat has the structure of an ordered monoid. This allows for tactics such as Unknown identifier `gcongr`gcongr to be applicable to the Chapter 2 natural numbers.

instance Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat where
  add_le_add_left a b hab c := (add_le_add_left a b c).mp hab

This illustration of the Unknown identifier `gcongr`gcongr tactic is not from the textbook.

example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hde: d < e) :
  a + d ≤ c + e := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chde:d < e⊢ a + d ≤ c + e
  gcongrh₁a:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chde:d < e⊢ a ≤ c
  orderAll goals completed! 🐙

Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5 Compare with Mathlib's Nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ m < n, p m) → p n) : p nNat.strong_induction_on.

theorem declaration uses 'sorry'Nat.strong_induction {m₀:Nat} {P: Nat → Prop}
  (hind: ∀ m, m ≥ m₀ → (∀ m', m₀ ≤ m' ∧ m' < m → P m') → P m) :
    ∀ m, m ≥ m₀ → P m := bym₀:NatP:Nat → Prophind:∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m⊢ ∀ m ≥ m₀, P m
  sorryAll goals completed! 🐙

Exercise 2.2.6 (backwards induction) Compare with Mathlib's Nat.decreasingInduction.{u_1} {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) {m : ℕ} (mn : m ≤ n) : motive m mnNat.decreasingInduction.

theorem declaration uses 'sorry'Nat.backwards_induction {n:Nat} {P: Nat → Prop}
  (hind: ∀ m, P (m++) → P m) (hn: P n) :
    ∀ m, m ≤ n → P m := byn:NatP:Nat → Prophind:∀ (m : Nat), P (m++) → P mhn:P n⊢ ∀ m ≤ n, P m
  sorryAll goals completed! 🐙

Exercise 2.2.7 (induction from a starting point) Compare with Mathlib's Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m ⋯) (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) (n : ℕ) (hmn : m ≤ n) : P n hmnNat.le_induction.

theorem declaration uses 'sorry'Nat.induction_from {n:Nat} {P: Nat → Prop} (hind: ∀ m, P m → P (m++)) :
    P n → ∀ m, m ≥ n → P m := byn:NatP:Nat → Prophind:∀ (m : Nat), P m → P (m++)⊢ P n → ∀ m ≥ n, P m
  sorryAll goals completed! 🐙

end Chapter2