Analysis I, Section 4.4: gaps in the rational numbers

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:

Irrationality of √2, and related facts about the rational numbers

Many of the results here can be established more quickly by relying more heavily on the Mathlib API; one can set oneself the exercise of doing so.

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)

Proposition 4.4.1 (Interspersing of integers by rationals) / Exercise 4.4.1

theorem declaration uses `sorry`Rat.between_int (x:ℚ) : ∃! n:ℤ, n ≤ x ∧ x < n+1 := byx:ℚ⊢ ∃! n, ↑n ≤ x ∧ x < ↑n + 1
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`Nat.exists_gt (x:ℚ) : ∃ n:ℕ, n > x := byx:ℚ⊢ ∃ n, ↑n > x
  sorryAll goals completed! 🐙

Proposition 4.4.3 (Interspersing of rationals)

theorem Rat.exists_between_rat {x y:ℚ} (h: x < y) : ∃ z:ℚ, x < z ∧ z < y := byx:ℚy:ℚh:x < y⊢ ∃ z, x < z ∧ z < y
  -- This proof is written to follow the structure of the original text.
  -- The reader is encouraged to find shorter proofs, for instance
  -- using Mathlib's `linarith` tactic.
  use (x+y)/2hx:ℚy:ℚh:x < y⊢ x < (x + y) / 2 ∧ (x + y) / 2 < y
  have h' : x/2 < y/2 := byx:ℚy:ℚh:x < y⊢ ∃ z, x < z ∧ z < y
    rw [show x/2 = x*(1/2) by ring, show y/2 = y*(1/2) by ring]x:ℚy:ℚh:x < y⊢ x * (1 / 2) < y * (1 / 2)
    apply mul_lt_mul_of_pos_right hx:ℚy:ℚh:x < y⊢ 0 < 1 / 2; positivityAll goals completed! 🐙
  constructorh.leftx:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ x < (x + y) / 2h.rightx:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ (x + y) / 2 < y
  .h.leftx:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ x < (x + y) / 2 convert add_lt_add_right h' (x/2) using 1h.e'_3x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ x = x / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ (x + y) / 2 = x / 2 + y / 2 <;>h.e'_3x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ x = x / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ (x + y) / 2 = x / 2 + y / 2 ringAll goals completed! 🐙
  convert add_lt_add_right h' (y/2) using 1h.e'_3x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ (x + y) / 2 = y / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ y = y / 2 + y / 2 <;>h.e'_3x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ (x + y) / 2 = y / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':x / 2 < y / 2⊢ y = y / 2 + y / 2 ringAll goals completed! 🐙

Exercise 4.4.2 (a)

theorem declaration uses `sorry`Nat.no_infinite_descent : ¬ ∃ a:ℕ → ℕ, ∀ n, a (n+1) < a n := by⊢ ¬∃ a, ∀ (n : ℕ), a (n + 1) < a n
  sorryAll goals completed! 🐙

Exercise 4.4.2 (b)

def declaration uses `sorry`Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) := by⊢ Decidable (∃ a, ∀ (n : ℕ), a (n + 1) < a n)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 4.4.2 (b)

def declaration uses `sorry`Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by⊢ Decidable (∃ a, ∀ (n : ℕ), a (n + 1) < a n)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

even_iff_exists_two_mul.{u_2} {α : Type u_2} [Semiring α] {a : α} : Even a ↔ ∃ b, a = 2 * b#check even_iff_exists_two_mul

even_iff_exists_two_mul.{u_2} {α : Type u_2} [Semiring α] {a : α} : Even a ↔ ∃ b, a = 2 * b

odd_iff_exists_bit1.{u_2} {α : Type u_2} [Semiring α] {a : α} : Odd a ↔ ∃ b, a = 2 * b + 1#check odd_iff_exists_bit1

odd_iff_exists_bit1.{u_2} {α : Type u_2} [Semiring α] {a : α} : Odd a ↔ ∃ b, a = 2 * b + 1

theorem declaration uses `sorry`Nat.even_or_odd'' (n:ℕ) : Even n ∨ Odd n := byn:ℕ⊢ Even n ∨ Odd n
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`Nat.not_even_and_odd (n:ℕ) : ¬ (Even n ∧ Odd n) := byn:ℕ⊢ ¬(Even n ∧ Odd n)
  sorryAll goals completed! 🐙

Nat.rec.{u} {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) :
  motive t#check Nat.rec

Nat.rec.{u} {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) :
  motive t

Proposition 4.4.4 / Exercise 4.4.3

theorem declaration uses `sorry`Rat.not_exist_sqrt_two : ¬ ∃ x:ℚ, x^2 = 2 := by⊢ ¬∃ x, x ^ 2 = 2
  -- This proof is written to follow the structure of the original text.
  by_contra hh:∃ x, x ^ 2 = 2⊢ False; choose x hx using hx:ℚhx:x ^ 2 = 2⊢ False
  have hnon : x ≠ 0 := by⊢ ¬∃ x, x ^ 2 = 2 aesopAll goals completed! 🐙
  wlog hpos : x > 0inrx:ℚhx:x ^ 2 = 2hnon:x ≠ 0this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ Falsex:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0⊢ False
  .inrx:ℚhx:x ^ 2 = 2hnon:x ≠ 0this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ False apply this _ _ _ (show -x>0 by⊢ ¬∃ x, x ^ 2 = 2 simpx:ℚhx:x ^ 2 = 2hnon:x ≠ 0this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ x < 0; orderAll goals completed! 🐙) <;>x:ℚhx:x ^ 2 = 2hnon:x ≠ 0this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ (-x) ^ 2 = 2x:ℚhx:x ^ 2 = 2hnon:x ≠ 0this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ -x ≠ 0 grindAll goals completed! 🐙
  have hrep : ∃ p q:ℕ, p > 0 ∧ q > 0 ∧ p^2 = 2*q^2 := by⊢ ¬∃ x, x ^ 2 = 2
    use x.num.toNat, x.denhx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0⊢ x.num.toNat > 0 ∧ x.den > 0 ∧ x.num.toNat ^ 2 = 2 * x.den ^ 2
    observe hnum_pos : x.num > 0hx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.num⊢ x.num.toNat > 0 ∧ x.den > 0 ∧ x.num.toNat ^ 2 = 2 * x.den ^ 2
    observe hden_pos : x.den > 0hx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.den⊢ x.num.toNat > 0 ∧ x.den > 0 ∧ x.num.toNat ^ 2 = 2 * x.den ^ 2
    refine ⟨ byx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.den⊢ x.num.toNat > 0 simp [hpos]All goals completed! 🐙, hden_pos, ?_ ⟩
    rw [←num_div_den x] at hxhx:ℚhx:(↑x.num / ↑x.den) ^ 2 = 2hnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.den⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2; field_simp at hxhx:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑x.num ^ 2 = ↑x.den ^ 2 * 2⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2
    have hnum_cast : x.num = x.num.toNat := Int.eq_natCast_toNat.mpr (byx:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑x.num ^ 2 = ↑x.den ^ 2 * 2⊢ 0 ≤ x.num positivityAll goals completed! 🐙)
    rw [hnum_cast] at hxhx:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑↑x.num.toNat ^ 2 = ↑x.den ^ 2 * 2hnum_cast:x.num = ↑x.num.toNat⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2; norm_cast at hxhx:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhnum_cast:x.num = ↑x.num.toNathx:x.num.toNat ^ 2 = x.den ^ 2 * 2⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2; grindAll goals completed! 🐙
  set P : ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p^2 = 2*q^2x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2⊢ False
  have hP : ∃ p, P p := by⊢ ¬∃ x, x ^ 2 = 2 aesopAll goals completed! 🐙
  have hiter (p:ℕ) (hPp: P p) : ∃ q, q < p ∧ P q := by⊢ ¬∃ x, x ^ 2 = 2
    obtain hp | hp := p.even_or_odd''inlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Even p⊢ ∃ q < p, P qinrx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Odd p⊢ ∃ q < p, P q
    .inlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Even p⊢ ∃ q < p, P q rw [even_iff_exists_two_mul] at hpinlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:∃ b, p = 2 * b⊢ ∃ q < p, P q
      obtain ⟨ k, rfl ⟩ := hpinlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)⊢ ∃ q < 2 * k, P q
      choose q hpos hq using hPp.2inlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2⊢ ∃ q < 2 * k, P q
      have : q^2 = 2 * k^2 := by⊢ ¬∃ x, x ^ 2 = 2 linarithAll goals completed! 🐙
      use qhx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:q ^ 2 = 2 * k ^ 2⊢ q < 2 * k ∧ P q; constructorh.leftx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:q ^ 2 = 2 * k ^ 2⊢ q < 2 * kh.rightx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:q ^ 2 = 2 * k ^ 2⊢ P q
      .h.leftx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:q ^ 2 = 2 * k ^ 2⊢ q < 2 * k sorryAll goals completed! 🐙
      exact ⟨ hpos, k, byx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pk:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:q ^ 2 = 2 * k ^ 2⊢ k > 0 linarith [hPp.1]All goals completed! 🐙, this ⟩
    have h1 : Odd (p^2) := by⊢ ¬∃ x, x ^ 2 = 2
      sorryAll goals completed! 🐙
    have h2 : Even (p^2) := by⊢ ¬∃ x, x ^ 2 = 2
      choose q hpos hq using hPp.2x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Odd ph1:Odd (p ^ 2)q:ℕhpos:q > 0hq:p ^ 2 = 2 * q ^ 2⊢ Even (p ^ 2)
      rw [even_iff_exists_two_mul]x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Odd ph1:Odd (p ^ 2)q:ℕhpos:q > 0hq:p ^ 2 = 2 * q ^ 2⊢ ∃ b, p ^ 2 = 2 * b
      use q^2All goals completed! 🐙
    observe : ¬(Even (p ^ 2) ∧ Odd (p ^ 2))inrx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P pp:ℕhPp:P php:Odd ph1:Odd (p ^ 2)h2:Even (p ^ 2)this:¬(Even (p ^ 2) ∧ Odd (p ^ 2))⊢ ∃ q < p, P q
    tautoAll goals completed! 🐙
  classical
  set f : ℕ → ℕ := fun p ↦ if hPp: P p then (hiter p hPp).choose else 0x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P phiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0⊢ False
  have hf (p:ℕ) (hPp: P p) : (f p < p) ∧ P (f p) := by⊢ ¬∃ x, x ^ 2 = 2
    simp [f, hPp]x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, P phiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0p:ℕhPp:P p⊢ ⋯.choose < p ∧ P ⋯.choose; exact (hiter p hPp).choose_specAll goals completed! 🐙
  choose p hP using hPx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0hf:∀ (p : ℕ), P p → f p < p ∧ P (f p)p:ℕhP:P p⊢ False
  set a : ℕ → ℕ := Nat.rec p (fun n p ↦ f p)x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0hf:∀ (p : ℕ), P p → f p < p ∧ P (f p)p:ℕhP:P pa:ℕ → ℕ := fun t ↦ Nat.rec p (fun n p ↦ f p) t⊢ False
  have ha (n:ℕ) : P (a n) := by⊢ ¬∃ x, x ^ 2 = 2
    induction n with
    | zero =>zerox:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0hf:∀ (p : ℕ), P p → f p < p ∧ P (f p)p:ℕhP:P pa:ℕ → ℕ := fun t ↦ Nat.rec p (fun n p ↦ f p) t⊢ P (a 0) exact hPAll goals completed! 🐙
    | succ n ih =>succx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0hf:∀ (p : ℕ), P p → f p < p ∧ P (f p)p:ℕhP:P pa:ℕ → ℕ := fun t ↦ Nat.rec p (fun n p ↦ f p) tn:ℕih:P (a n)⊢ P (a (n + 1)) exact (hf _ ih).2All goals completed! 🐙
  have hlt (n:ℕ) : a (n+1) < a n := by⊢ ¬∃ x, x ^ 2 = 2
    have : a (n+1) = f (a n) := n.rec_add_one p (fun n p ↦ f p)x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2P:ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ), P p → ∃ q < p, P qf:ℕ → ℕ := fun p ↦ if hPp : P p then ⋯.choose else 0hf:∀ (p : ℕ), P p → f p < p ∧ P (f p)p:ℕhP:P pa:ℕ → ℕ := fun t ↦ Nat.rec p (fun n p ↦ f p) tha:∀ (n : ℕ), P (a n)n:ℕthis:a (n + 1) = f (a n)⊢ a (n + 1) < a n
    grindAll goals completed! 🐙
  exact Nat.no_infinite_descent ⟨ a, hlt ⟩All goals completed! 🐙

Proposition 4.4.5

theorem Rat.exist_approx_sqrt_two {ε:ℚ} (hε:ε>0) : ∃ x ≥ (0:ℚ), x^2 < 2 ∧ 2 < (x+ε)^2 := byε:ℚhε:ε > 0⊢ ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2
  -- This proof is written to follow the structure of the original text.
  by_contra! hε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2⊢ False
  have (n:ℕ): (n*ε)^2 < 2 := byε:ℚhε:ε > 0⊢ ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2
    induction' n with n hnzeroε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2⊢ (↑0 * ε) ^ 2 < 2succε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ (↑(n + 1) * ε) ^ 2 < 2; simpsuccε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ (↑(n + 1) * ε) ^ 2 < 2
    simp [add_mul]succε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ (↑n * ε + ε) ^ 2 < 2
    apply lt_of_le_of_ne (h (n*ε) (byε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ ↑n * ε ≥ 0 positivityAll goals completed! 🐙) hn)
    have := not_exist_sqrt_twosuccε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2this:¬∃ x, x ^ 2 = 2⊢ (↑n * ε + ε) ^ 2 ≠ 2
    aesopAll goals completed! 🐙
  choose n hn using Nat.exists_gt (2/ε)ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:↑n > 2 / ε⊢ False
  rw [gt_iff_lt, div_lt_iff₀', mul_comm, ←sq_lt_sq₀] at hnε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falsehaε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2hbε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 / ε < ↑n⊢ 0 < ε <;>ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falsehaε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2hbε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * ε) ^ 2 < 2n:ℕhn:2 / ε < ↑n⊢ 0 < ε try positivityAll goals completed! 🐙
  grindAll goals completed! 🐙

/-- Example 4.4.6 -/
example :
  let ε:ℚ := 1/1000
  let x:ℚ := 1414/1000
  x^2 < 2 ∧ 2 < (x+ε)^2 := by⊢ let ε := 1 / 1000;
let x := 1414 / 1000;
x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2 norm_numAll goals completed! 🐙