Gaps in the rational numbers

Аналіз I, Розділ 4.4: Прогалини у раціональних числах

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні побудови та результати цього розділу:

Ірраціональність √2 та пов’язані факти про раціональні числа

Багато результатів тут можна встановити швидше, більше спираючись на API Mathlib; можна поставити собі вправу зробити це.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

Твердження 4.4.1 (Переплетення цілих чисел раціональними) / Вправа 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! 🐙

Твердження 4.4.3 (Переплетення раціональних чисел)

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
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  -- Читача заохочують знаходити коротші доведення, наприклад,
  -- використовуючи тактику `linarith` з Mathlib.
  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':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x < (x + y) / 2h.rightx:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 < y
  .h.leftx:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x < (x + y) / 2 convert add_lt_add_right h' (x/2) using 1h.e'_3x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x = x / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = y / 2 + x / 2 <;>h.e'_3x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ x = x / 2 + x / 2h.e'_4x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = y / 2 + x / 2 ringAll goals completed! 🐙
  convert add_lt_add_right h' (y/2) using 1h.e'_3x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = x / 2 + y / 2h.e'_4x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ y = y / 2 + y / 2 <;>h.e'_3x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ (x + y) / 2 = x / 2 + y / 2h.e'_4x:ℚy:ℚh:x < yh':_fvar.1893 / 2 < _fvar.1894 / 2 := ?_mvar.2194⊢ y = y / 2 + y / 2 ringAll goals completed! 🐙

Вправа 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! 🐙

Вправа 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)
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа 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)
  -- перший рядок цієї побудови має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll 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 := 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

Твердження 4.4.4 / Вправа 4.4.3

theorem declaration uses 'sorry'Rat.not_exist_sqrt_two : ¬ ∃ x:ℚ, x^2 = 2 := by⊢ ¬∃ x, x ^ 2 = 2
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  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:_fvar.9150 ≠ 0 := ?_mvar.9193this:∀ (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:_fvar.9150 ≠ 0 := ?_mvar.9193this:∀ (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:_fvar.9150 ≠ 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.9154)this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ x < 0; orderAll goals completed! 🐙) <;>x:ℚhx:x ^ 2 = 2hnon:_fvar.9150 ≠ 0 := ?_mvar.9193this:∀ (x : ℚ), x ^ 2 = 2 → x ≠ 0 → x > 0 → Falsehpos:¬x > 0⊢ (-x) ^ 2 = 2x:ℚhx:x ^ 2 = 2hnon:_fvar.9150 ≠ 0 := ?_mvar.9193this:∀ (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 = 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 (byx:ℚhnon:x ≠ 0hpos:x > 0hnum_pos:0 < x.numhden_pos:0 < x.denhx:↑x.num ^ 2 = 2 * ↑x.den ^ 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 = 2 * ↑x.den ^ 2hnum_cast:x.num = ↑x.num.toNat⊢ x.num.toNat ^ 2 = 2 * x.den ^ 2; norm_cast at hxAll goals completed! 🐙
  set P : ℕ → Prop := fun p ↦ p > 0 ∧ ∃ q > 0, p^2 = 2*q^2x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:Even p⊢ ∃ q < p, P qinrx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:Odd p⊢ ∃ q < p, P q
    .inlx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕ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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:∃ b, p = 2 * b⊢ ∃ q < p, P q
      obtain ⟨ k, rfl ⟩ := hpinl.introx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕhPp:P (2 * k)⊢ ∃ q < 2 * k, P q
      choose q hpos hq using hPp.2inl.introx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕ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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.96194 ^ 2 = 2 * _fvar.96167 ^ 2 := ?_mvar.96894⊢ q < 2 * k ∧ P q; constructorh.leftx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.96194 ^ 2 = 2 * _fvar.96167 ^ 2 := ?_mvar.96894⊢ q < 2 * kh.rightx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.96194 ^ 2 = 2 * _fvar.96167 ^ 2 := ?_mvar.96894⊢ P q
      .h.leftx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos✝:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.96194 ^ 2 = 2 * _fvar.96167 ^ 2 := ?_mvar.96894⊢ 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 ^ 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.80061 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.19644))))k:ℕhPp:P (2 * k)q:ℕhpos:q > 0hq:(2 * k) ^ 2 = 2 * q ^ 2this:_fvar.96194 ^ 2 = 2 * _fvar.96167 ^ 2 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (_fvar.96194 ^ 2) (2 * _fvar.96167 ^ 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.96167)
                        (Mathlib.Tactic.Ring.add_mul
                          (Mathlib.Tactic.Ring.mul_add
                            (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96167) (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.96167 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
                          (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96167 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ 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.96167 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))
                        (Mathlib.Tactic.Ring.add_mul
                          (Mathlib.Tactic.Ring.mul_add
                            (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96167) (Nat.rawCast 2)
                              (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 4)))
                            (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0)))
                          (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ 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.96194)
                        (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.96194 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96194) (Nat.rawCast 2)
                                (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                              (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))
                      (Mathlib.Tactic.Ring.add_mul
                        (Mathlib.Tactic.Ring.mul_add
                          (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96194) (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.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))
                        (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul (↑_fvar.96194) (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.96167 ^ Nat.rawCast 2 * Nat.rawCast 4)
                        (Mathlib.Tactic.Ring.add_pf_zero_add
                          (↑_fvar.96194 ^ 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.96167 ^ Nat.rawCast 2 * Nat.rawCast 4 +
                        (↑_fvar.96194 ^ 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.96194)
                        (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.96194 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96194) (Nat.rawCast 2)
                                (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                              (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ 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.96194 ^ 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.96167)
                        (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.96167 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96167) (Nat.rawCast 2)
                                (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                              (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))
                      (Mathlib.Tactic.Ring.add_mul
                        (Mathlib.Tactic.Ring.mul_add
                          (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96167) (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.96167 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))
                        (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul (↑_fvar.96167) (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.96167 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast)
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ 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.96167) (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.96194) (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.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))
                        (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.96167 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast)
                          (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.96194 ^ 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.96167 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast +
                            (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))))
                    (Mathlib.Tactic.Ring.zero_mul
                      (Nat.rawCast 1 +
                        (↑_fvar.96167 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast +
                          (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.add_pf_add_zero
                      (Nat.rawCast 2 +
                        (↑_fvar.96167 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast +
                          (↑_fvar.96194 ^ 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.96167) (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.96194) (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.96167) ^ 2) (2 * _fvar.96194 ^ 2))
                      (congr
                        (congrArg Eq
                          (Eq.trans (Nat.cast_pow (2 * _fvar.96167) 2)
                            (congrArg (fun x => x ^ 2) (Nat.cast_mul 2 _fvar.96167))))
                        (Eq.trans (Nat.cast_mul 2 (_fvar.96194 ^ 2))
                          (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.96194 2)))))
                    _fvar.96206))))
            (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.96194 ^ 2) (2 * _fvar.96167 ^ 2))
                        (congr (congrArg LT.lt (Nat.cast_pow _fvar.96194 2))
                          (Eq.trans (Nat.cast_mul 2 (_fvar.96167 ^ 2))
                            (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.96167 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.96167)
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96167) (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.96167 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96167 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ 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.96167 ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96167) (Nat.rawCast 2)
                                (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 4)))
                              (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ 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.96194)
                          (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.96194 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_mul
                              (Mathlib.Tactic.Ring.mul_add
                                (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96194) (Nat.rawCast 2)
                                  (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                                (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1))
                                (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))
                        (Mathlib.Tactic.Ring.add_mul
                          (Mathlib.Tactic.Ring.mul_add
                            (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96194) (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.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))
                          (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))
                      (Mathlib.Tactic.Ring.sub_pf
                        (Mathlib.Tactic.Ring.neg_add
                          (Mathlib.Tactic.Ring.neg_mul (↑_fvar.96194) (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.96167 ^ Nat.rawCast 2 * Nat.rawCast 4)
                          (Mathlib.Tactic.Ring.add_pf_zero_add
                            (↑_fvar.96194 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0)))))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑_fvar.96167) (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.96194) (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.96167 ^ Nat.rawCast 2 * (Int.negOfNat 4).rawCast +
                        (↑_fvar.96194 ^ 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.96167)
                          (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.96167 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_mul
                              (Mathlib.Tactic.Ring.mul_add
                                (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96167) (Nat.rawCast 2)
                                  (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                                (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1))
                                (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))
                        (Mathlib.Tactic.Ring.add_mul
                          (Mathlib.Tactic.Ring.mul_add
                            (Mathlib.Tactic.Ring.mul_pf_right (↑_fvar.96167) (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.96167 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0)))
                          (Mathlib.Tactic.Ring.zero_mul (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96167 ^ 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.96167 ^ Nat.rawCast 2 * Nat.rawCast 2 + 0))))
                    (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.96194)
                      (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.96194 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                        (Mathlib.Tactic.Ring.add_mul
                          (Mathlib.Tactic.Ring.mul_add
                            (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.96194) (Nat.rawCast 2)
                              (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                            (Mathlib.Tactic.Ring.mul_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                          (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
                          (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.96194 ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul (↑_fvar.96194) (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.96167 ^ Nat.rawCast 2 * Nat.rawCast 2)
                          (Mathlib.Tactic.Ring.add_pf_zero_add
                            (↑_fvar.96194 ^ 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.96167) (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.96194) (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.96194 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0)))
                        (Mathlib.Tactic.Ring.add_pf_add_lt (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4)
                          (Mathlib.Tactic.Ring.add_pf_zero_add
                            (↑_fvar.96194 ^ 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.96167 ^ Nat.rawCast 2 * Nat.rawCast 4 +
                            (↑_fvar.96194 ^ Nat.rawCast 2 * (Int.negOfNat 2).rawCast + 0)))))
                    (Mathlib.Tactic.Ring.zero_mul
                      (Nat.rawCast 1 +
                        (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 2 +
                          (↑_fvar.96194 ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))
                    (Mathlib.Tactic.Ring.add_pf_add_zero
                      (Nat.rawCast 2 +
                        (↑_fvar.96167 ^ Nat.rawCast 2 * Nat.rawCast 4 +
                          (↑_fvar.96194 ^ 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.96167) (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.96194) (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.96167) ^ 2) (2 * _fvar.96194 ^ 2))
                        (congr
                          (congrArg Eq
                            (Eq.trans (Nat.cast_pow (2 * _fvar.96167) 2)
                              (congrArg (fun x => x ^ 2) (Nat.cast_mul 2 _fvar.96167))))
                          (Eq.trans (Nat.cast_mul 2 (_fvar.96194 ^ 2))
                            (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.96194 2)))))
                      _fvar.96206)))))
            (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.96167 ^ 2) (_fvar.96194 ^ 2))
                        (congr
                          (congrArg LT.lt
                            (Eq.trans (Nat.cast_mul 2 (_fvar.96167 ^ 2))
                              (congrArg (HMul.hMul 2) (Nat.cast_pow _fvar.96167 2))))
                          (Nat.cast_pow _fvar.96194 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 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:Odd ph1:Odd (_fvar.95894 ^ 2) := ?_mvar.109698q:ℕ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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:Odd ph1:Odd (_fvar.95894 ^ 2) := ?_mvar.109698q:ℕ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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146p:ℕhPp:P php:Odd ph1:Odd (_fvar.95894 ^ 2) := ?_mvar.109698h2:Even (_fvar.95894 ^ 2) := ?_mvar.110021this:¬(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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → 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.80146hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.80061 p), @_fvar.118352 p < p ∧ @_fvar.80061 (@_fvar.118352 p) := fun p hPp => @?_mvar.118475 p hPpp:ℕhP:P p⊢ False
  set a : ℕ → ℕ := Nat.rec p (fun n p ↦ f p)x:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.80061 p), @_fvar.118352 p < p ∧ @_fvar.80061 (@_fvar.118352 p) := fun p hPp => @?_mvar.118475 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.119232 (fun n p => @_fvar.118352 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.80061 p), @_fvar.118352 p < p ∧ @_fvar.80061 (@_fvar.118352 p) := fun p hPp => @?_mvar.118475 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.119232 (fun n p => @_fvar.118352 p) t⊢ P (a 0) exact hPAll goals completed! 🐙
    | succ n ih =>succx:ℚhx:x ^ 2 = 2hnon:x ≠ 0hpos:x > 0hrep:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.80061 p), @_fvar.118352 p < p ∧ @_fvar.80061 (@_fvar.118352 p) := fun p hPp => @?_mvar.118475 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.119232 (fun n p => @_fvar.118352 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:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.19643P:ℕ → Prop := fun p => p > 0 ∧ ∃ q > 0, p ^ 2 = 2 * q ^ 2hiter:∀ (p : ℕ) (hPp : @_fvar.80061 p), ∃ q < p, @_fvar.80061 q := fun p hPp => @?_mvar.95911 p hPpf:ℕ → ℕ := fun p => if hPp : @_fvar.80061 p then Exists.choose (@_fvar.95912 p hPp) else 0hf:∀ (p : ℕ) (hPp : @_fvar.80061 p), @_fvar.118352 p < p ∧ @_fvar.80061 (@_fvar.118352 p) := fun p hPp => @?_mvar.118475 p hPpp:ℕhP:P pa:ℕ → ℕ := fun t => Nat.rec _fvar.119232 (fun n p => @_fvar.118352 p) tha:(n : ℕ) → @_fvar.80061 (@_fvar.119270 n) := fun n => @?_mvar.119411 nn:ℕthis:@_fvar.119270 (_fvar.119501 + 1) = @_fvar.118352 (@_fvar.119270 _fvar.119501) := ?_mvar.120063⊢ a (n + 1) < a n
    grindAll goals completed! 🐙
  exact Nat.no_infinite_descent ⟨ a, hlt ⟩All goals completed! 🐙

Твердження 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
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  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:?_mvar.143689 := Rat.not_exist_sqrt_two⊢ (↑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 * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕ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 * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falsehaε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2hbε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 / ε < ↑n⊢ 0 < ε <;>ε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 ^ 2 < (↑n * ε) ^ 2⊢ Falsehaε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ 2hbε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 < ↑n * ε⊢ 0 ≤ ↑n * εε:ℚhε:ε > 0h:∀ x ≥ 0, x ^ 2 < 2 → (x + ε) ^ 2 ≤ 2this:∀ (n : ℕ), (↑n * _fvar.137422) ^ 2 < 2 := fun n => @?_mvar.139670 nn:ℕhn:2 / ε < ↑n⊢ 0 < ε try positivityAll goals completed! 🐙
  grindAll goals completed! 🐙

Приклад 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! 🐙