Gaps in the rational numbers

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 := x:ℚ⊢ ∃! n, ↑n ≤ x ∧ x < ↑n + 1 All goals completed! 🐙
theorem declaration uses 'sorry'Nat.exists_gt (x:ℚ) : ∃ n:ℕ, n > x := x:ℚ⊢ ∃ n, ↑n > x All goals completed! 🐙

Proposition 4.4.3 (Interspersing of rationals)

theorem Rat.exists_between_rat {x y:ℚ} (h: x < y) : ∃ z:ℚ, x < z ∧ z < y := x:ℚ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. x:ℚy:ℚh:x < y⊢ x < (x + y) / 2 ∧ (x + y) / 2 < y have h' : x/2 < y/2 := x:ℚy:ℚh:x < y⊢ ∃ z, x < z ∧ z < y x:ℚy:ℚh:x < y⊢ x * (1 / 2) < y * (1 / 2) x:ℚy:ℚh:x < y⊢ 0 < 1 / 2; All goals completed! 🐙 x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x < (x + y) / 2x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 < y x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x < (x + y) / 2 x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x = x / 2 + x / 2x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = y / 2 + x / 2 x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x = x / 2 + x / 2x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = y / 2 + x / 2 All goals completed! 🐙 x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = x / 2 + y / 2x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ y = y / 2 + y / 2 x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = x / 2 + y / 2x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ y = y / 2 + y / 2 All goals completed! 🐙

Exercise 4.4.2

theorem declaration uses 'sorry'Nat.no_infinite_descent : ¬ ∃ a:ℕ → ℕ, ∀ n, a (n+1) < a n := ⊢ ¬∃ a, ∀ (n : ℕ), a (n + 1) < a n All goals completed! 🐙
def declaration uses 'sorry'Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) := ⊢ Decidable (∃ a, ∀ (n : ℕ), a (n + 1) < a n) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. All goals completed! 🐙
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
theorem declaration uses 'sorry'Nat.even_or_odd'' (n:ℕ) : Even n ∨ Odd n := n:ℕ⊢ Even n ∨ Odd n All goals completed! 🐙theorem declaration uses 'sorry'Nat.not_even_and_odd (n:ℕ) : ¬ (Even n ∧ Odd n) := n:ℕ⊢ ¬(Even n ∧ Odd n) All goals completed! 🐙
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 := ⊢ ¬∃ x, x ^ 2 = 2 -- This proof is written to follow the structure of the original text. h:∃ x, x ^ 2 = 2⊢ False; x:ℚhx:x ^ 2 = 2⊢ False have hnon : x ≠ 0 := ⊢ ¬∃ x, x ^ 2 = 2 All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:_fvar.8898 ≠ 0 := ?_mvar.8941this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ Falsex:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0⊢ False x:ℚhx:x ^ 2 = 2hnon:_fvar.8898 ≠ 0 := ?_mvar.8941this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ False apply this _ _ _ (show -x>0 ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:_fvar.8898 ≠ 0 := id (Aesop.BuiltinRules.not_intro fun a => Eq.ndrec (motive := fun x => x ^ 2 = 2 → False) (fun hx => False.elim (Eq.mp (Eq.trans (congrArg (fun x => x = 2) (zero_pow (of_eq_true (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true)))) (OfNat.zero_ne_ofNat._simp_1 2)) hx)) (Eq.symm a) _fvar.8902)this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ x < 0; All goals completed! 🐙) x:ℚhx:x ^ 2 = 2hnon:_fvar.8898 ≠ 0 := ?_mvar.8941this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ (-x) ^ 2 = 2x:ℚhx:x ^ 2 = 2hnon:_fvar.8898 ≠ 0 := ?_mvar.8941this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ -x ≠ 0 All goals completed! 🐙 have hrep : ∃ p q:ℕ, p > 0 ∧ q > 0 ∧ p^2 = 2*q^2 := ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0⊢ x.num.toNat > 0 ∧ x.den > 0 ∧ x.num.toNat ^ 2 = 2 * x.den ^ 2 x:ℚ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 x:ℚ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 ⟨ x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.den⊢ x.num.toNat > 0 All goals completed! 🐙, hden_pos, ?_ ⟩ x:ℚ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; x:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑x.num ^ 2 = 2 * ↑x.den ^ 2⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2 have hnum_cast : x.num = x.num.toNat := Int.eq_natCast_toNat.mpr (x:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑x.num ^ 2 = 2 * ↑x.den ^ 2⊢ 0 ≤ x.num All goals completed! 🐙) x:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑↑x.num.toNat ^ 2 = 2 * ↑x.den ^ 2hnum_cast:x.num = ↑x.num.toNat⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2; All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2⊢ False have hP : ∃ p, P p := ⊢ ¬∃ x, x ^ 2 = 2 All goals completed! 🐙 have hiter (p:ℕ) (hPp: P p) : ∃ q, q < p ∧ P q := ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Even p⊢ ∃ q < p, P qx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Odd p⊢ ∃ q < p, P q x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Even p⊢ ∃ q < p, P q x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:∃ b, p = 2 * b⊢ ∃ q < p, P q x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕhPp:P (2 * k)⊢ ∃ q < 2 * k, P q x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕ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 := ⊢ ¬∃ x, x ^ 2 = 2 All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.95942 ^ 2 = 2 * _fvar.95915 ^ 2 := ?_mvar.96642⊢ q < 2 * k ∧ P q; x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.95942 ^ 2 = 2 * _fvar.95915 ^ 2 := ?_mvar.96642⊢ q < 2 * kx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.95942 ^ 2 = 2 * _fvar.95915 ^ 2 := ?_mvar.96642⊢ P q x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.95942 ^ 2 = 2 * _fvar.95915 ^ 2 := ?_mvar.96642⊢ q < 2 * k All goals completed! 🐙 exact ⟨ hpos, k, x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:∃ p q, p > 0 ∧ q > 0 ∧ p ^ 2 = 2 * q ^ 2 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:∃ p, @_fvar.79809 p := of_eq_true (Eq.trans (congrArg Exists (funext fun p => congrFun (funext fun p => congr (congrArg And gt_iff_lt._simp_1) (congrArg Exists (funext fun q => congrArg (fun x => x ∧ p ^ 2 = 2 * q ^ 2) gt_iff_lt._simp_1))) p)) (eq_true (id (Eq.mp (congrArg Exists (funext fun p => Eq.trans (congrArg Exists (funext fun q => congr (congrArg And gt_iff_lt._simp_1) (congrArg (fun x => x ∧ p ^ 2 = 2 * q ^ 2) gt_iff_lt._simp_1))) exists_and_left._simp_1)) _fvar.19392))))k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.95942 ^ 2 = 2 * _fvar.95915 ^ 2 := Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (_fvar.95942 ^ 2) (2 * _fvar.95915 ^ 2) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95915) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0))))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95942) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95942 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95942) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95942 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95915) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_gt (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2)) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 4))))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast + (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast + (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 4)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 ((2 * _fvar.95915) ^ 2) (2 * _fvar.95942 ^ 2)) (congr (congrArg Eq (Eq.trans (Nat.cast_pow (2 * _fvar.95915) 2) (congrArg (fun x => x ^ 2) (Nat.cast_mul 2 _fvar.95915)))) (Eq.trans (Nat.cast_mul 2 (_fvar.95942 ^ 2)) (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.95942 2))))) _fvar.95954)))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 (_fvar.95942 ^ 2) (2 * _fvar.95915 ^ 2)) (congr (congrArg LT.lt (Nat.cast_pow _fvar.95942 2)) (Eq.trans (Nat.cast_mul 2 (_fvar.95915 ^ 2)) (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.95915 2))))) a)))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false)))))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95915) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 2) (Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0))))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95942) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95942 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 4)) (Eq.refl (Int.negOfNat 4)))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 2))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95915 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast + (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95915) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95915 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.95942) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.mul_pow (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 2)) (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))) (Mathlib.Tactic.Ring.pow_zero (↑_fvar.95942 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0)))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2)) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2) (Eq.refl 4)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0))))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 2 + (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 2 + (↑_fvar.95915 ^ Nat.rawCast 2 * Nat.rawCast 4 + (↑_fvar.95942 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.95915) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 4)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 4)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.95942) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (neg_eq_zero.mpr (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 ((2 * _fvar.95915) ^ 2) (2 * _fvar.95942 ^ 2)) (congr (congrArg Eq (Eq.trans (Nat.cast_pow (2 * _fvar.95915) 2) (congrArg (fun x => x ^ 2) (Nat.cast_mul 2 _fvar.95915)))) (Eq.trans (Nat.cast_mul 2 (_fvar.95942 ^ 2)) (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.95942 2))))) _fvar.95954))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 (2 * _fvar.95915 ^ 2) (_fvar.95942 ^ 2)) (congr (congrArg LT.lt (Eq.trans (Nat.cast_mul 2 (_fvar.95915 ^ 2)) (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.95915 2)))) (Nat.cast_pow _fvar.95942 2))) a)))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))))))⊢ k > 0 All goals completed! 🐙, this ⟩ have h1 : Odd (p^2) := ⊢ ¬∃ x, x ^ 2 = 2 All goals completed! 🐙 have h2 : Even (p^2) := ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Odd ph1:Odd (_fvar.95642 ^ 2) := ?_mvar.109446q:ℕhpos:q > 0hq:p ^ 2 = 2 * q ^ 2⊢ Even (p ^ 2) x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Odd ph1:Odd (_fvar.95642 ^ 2) := ?_mvar.109446q:ℕhpos:q > 0hq:p ^ 2 = 2 * q ^ 2⊢ ∃ b, p ^ 2 = 2 * b All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894p:ℕhPp:P php:Odd ph1:Odd (_fvar.95642 ^ 2) := ?_mvar.109446h2:Even (_fvar.95642 ^ 2) := ?_mvar.109769this:¬(Even (p ^ 2) ∧ Odd (p ^ 2))⊢ ∃ q < p, P q All goals completed! 🐙 classical x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0⊢ False have hf (p:ℕ) (hPp: P p) : (f p < p) ∧ P (f p) := ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hP:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.79894hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0p:ℕhPp:P p⊢ ⋯.choose < p ∧ P ⋯.choose; All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.79809 p), @_fvar.118100 p < p ∧ @_fvar.79809 (@_fvar.118100 p) := fun p hPp => @?_mvar.118223 p hPpp:ℕhP:P p⊢ False x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.79809 p), @_fvar.118100 p < p ∧ @_fvar.79809 (@_fvar.118100 p) := fun p hPp => @?_mvar.118223 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.118980 (fun n p => @_fvar.118100 p) t⊢ False have ha (n:ℕ) : P (a n) := ⊢ ¬∃ x, x ^ 2 = 2 induction n with x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.79809 p), @_fvar.118100 p < p ∧ @_fvar.79809 (@_fvar.118100 p) := fun p hPp => @?_mvar.118223 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.118980 (fun n p => @_fvar.118100 p) t⊢ P (a 0) All goals completed! 🐙 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.79809 p), @_fvar.118100 p < p ∧ @_fvar.79809 (@_fvar.118100 p) := fun p hPp => @?_mvar.118223 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.118980 (fun n p => @_fvar.118100 p) tn:ℕih:P (a n)⊢ P (a (n + 1)) All goals completed! 🐙 have hlt (n:ℕ) : a (n+1) < a n := ⊢ ¬∃ x, x ^ 2 = 2 x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19391P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.79809 p), ∃ q < p, @_fvar.79809 q := fun p hPp => @?_mvar.95659 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.79809 p then Exists.choose (@_fvar.95660 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.79809 p), @_fvar.118100 p < p ∧ @_fvar.79809 (@_fvar.118100 p) := fun p hPp => @?_mvar.118223 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.118980 (fun n p => @_fvar.118100 p) tha:(n : ℕ) → @_fvar.79809 (@_fvar.119018 n) := fun n => @?_mvar.119159 nn:ℕthis:@_fvar.119018 (_fvar.119249 + 1) = @_fvar.118100 (@_fvar.119018 _fvar.119249) := ?_mvar.119811⊢ a (n + 1) < a n All goals completed! 🐙 All goals completed! 🐙

Proposition 4.4.5

theorem Rat.exist_approx_sqrt_two {ε:ℚ} (hε:ε>0) : ∃ x ≥ (0:ℚ), x^2 < 2 ∧ 2 < (x+ε)^2 := ε:ℚhε:ε > 0⊢ ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2 -- This proof is written to follow the structure of the original text. ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2⊢ False have (n:ℕ): (n*ε)^2 < 2 := ε:ℚhε:ε > 0⊢ ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2 ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2⊢ (↑0 * ε) ^ 2 < 2ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ (↑(n + 1) * ε) ^ 2 < 2; ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ (↑(n + 1) * ε) ^ 2 < 2 ε:ℚ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*ε) (ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2⊢ ↑n * ε ≥ 0 All goals completed! 🐙) hn) ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2n:ℕhn:(↑n * ε) ^ 2 < 2this:?_mvar.143437 := Rat.not_exist_sqrt_two⊢ (↑n * ε + ε) ^ 2 ≠ 2 All goals completed! 🐙 ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:↑n > 2 / ε⊢ False ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falseε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 / ε < ↑n⊢ 0 < ε ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falseε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137170) ^ 2 < 2 := fun n => @?_mvar.139418 nn:ℕhn:2 / ε < ↑n⊢ 0 < ε try All goals completed! 🐙 All goals completed! 🐙

Example 4.4.6

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