The least upper bound property

Аналіз I, Розділ 5.5: Властивість найменшої верхньої межі

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

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

  • Верхня межа та найменша верхня межа на дійсній прямій

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

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

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

namespace Chapter5

Визначення 5.5.1 (верхні межі). Тут ми використовуємо множину upperBounds.{u_1} {α : Type u_1} [LE α] (s : Set α) : Set αupperBounds, визначену в Mathlib.

theorem Real.upperBound_def (E: Set Real) (M: Real) : M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M := mem_upperBounds
theorem Real.lowerBound_def (E: Set Real) (M: Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M := mem_lowerBounds

API для Приклада 5.5.2

theorem Real.Icc_def (x y:Real) : .Icc x y = { z | x ≤ z ∧ z ≤ y } := rfl

API для Приклада 5.5.2

theorem Real.mem_Icc (x y z:Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y := x:Realy:Realz:Real⊢ z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y All goals completed! 🐙

Приклад 5.5.2

declaration uses 'sorry'example (M: Real) : M ∈ upperBounds (.Icc 0 1) ↔ M ≥ 1 := M:Real⊢ M ∈ upperBounds (Set.Icc 0 1) ↔ M ≥ 1 All goals completed! 🐙

API для Приклада 5.5.3

theorem Real.Ioi_def (x:Real) : .Ioi x = { z | z > x } := rfl

Приклад 5.5.3

declaration uses 'sorry'example : ¬ ∃ M : Real, M ∈ upperBounds (.Ioi 0) := ⊢ ¬∃ M, M ∈ upperBounds (Set.Ioi 0) All goals completed! 🐙

Приклад 5.5.4

declaration uses 'sorry'example : ∀ M, M ∈ upperBounds (∅ : Set Real) := ⊢ ∀ (M : Real), M ∈ upperBounds ∅ All goals completed! 🐙
theorem declaration uses 'sorry'Real.upperBound_upper {M M': Real} (h: M ≤ M') {E: Set Real} (hb: M ∈ upperBounds E) : M' ∈ upperBounds E := M:RealM':Realh:M ≤ M'E:Set Realhb:M ∈ upperBounds E⊢ M' ∈ upperBounds E All goals completed! 🐙

Визначення 5.5.5 (найменша верхня межа). Тут ми використовуємо предикат Unknown identifier `isLUB`isLUB, визначений у Mathlib.

theorem Real.isLUB_def (E: Set Real) (M: Real) : IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M := E:Set RealM:Real⊢ IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M All goals completed! 🐙
theorem Real.isGLB_def (E: Set Real) (M: Real) : IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M := E:Set RealM:Real⊢ IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M All goals completed! 🐙

Приклад 5.5.6

declaration uses 'sorry'example : IsLUB (.Icc 0 1) (1 : Real) := ⊢ IsLUB (Set.Icc 0 1) 1 All goals completed! 🐙

Приклад 5.5.7

declaration uses 'sorry'example : ¬∃ M, IsLUB (∅: Set Real) M := ⊢ ¬∃ M, IsLUB ∅ M All goals completed! 🐙

Твердження 5.5.8 (Єдиність найменшої верхньої межі)

theorem Real.LUB_unique {E: Set Real} {M M': Real} (h1: IsLUB E M) (h2: IsLUB E M') : M = M' := E:Set RealM:RealM':Realh1:IsLUB E Mh2:IsLUB E M'⊢ M = M' All goals completed! 🐙

Визначення "обмежено зверху" з використанням нотації Mathlib

theorem Real.bddAbove_def (E: Set Real) : BddAbove E ↔ ∃ M, M ∈ upperBounds E := Set.nonempty_def
theorem Real.bddBelow_def (E: Set Real) : BddBelow E ↔ ∃ M, M ∈ lowerBounds E := Set.nonempty_def

Вправа 5.5.2

theorem declaration uses 'sorry'Real.upperBound_between {E: Set Real} {n:ℕ} {L K:ℤ} (hLK: L < K) (hK: K*((1/(n+1):ℚ):Real) ∈ upperBounds E) (hL: L*((1/(n+1):ℚ):Real) ∉ upperBounds E) : ∃ m, L < m ∧ m ≤ K ∧ m*((1/(n+1):ℚ):Real) ∈ upperBounds E ∧ (m-1)*((1/(n+1):ℚ):Real) ∉ upperBounds E := E:Set Realn:ℕL:ℤK:ℤhLK:L < KhK:↑K * ↑(1 / (↑n + 1)) ∈ upperBounds EhL:↑L * ↑(1 / (↑n + 1)) ∉ upperBounds E⊢ ∃ m, L < m ∧ m ≤ K ∧ ↑m * ↑(1 / (↑n + 1)) ∈ upperBounds E ∧ (↑m - 1) * ↑(1 / (↑n + 1)) ∉ upperBounds E All goals completed! 🐙

Вправа 5.5.3

theorem declaration uses 'sorry'Real.upperBound_discrete_unique {E: Set Real} {n:ℕ} {m m':ℤ} (hm1: (((m:ℚ) / (n+1):ℚ):Real) ∈ upperBounds E) (hm2: (((m:ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∉ upperBounds E) (hm'1: (((m':ℚ) / (n+1):ℚ):Real) ∈ upperBounds E) (hm'2: (((m':ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∉ upperBounds E) : m = m' := E:Set Realn:ℕm:ℤm':ℤhm1:↑(↑m / (↑n + 1)) ∈ upperBounds Ehm2:↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehm'1:↑(↑m' / (↑n + 1)) ∈ upperBounds Ehm'2:↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E⊢ m = m' All goals completed! 🐙

Леми можуть бути корисними для доведення 5.5.4

theorem declaration uses 'sorry'Sequence.IsCauchy.abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy): ((|a| : ℕ → ℚ) : Sequence).IsCauchy := a:ℕ → ℚha:(↑a).IsCauchy⊢ (↑|a|).IsCauchy All goals completed! 🐙
theorem declaration uses 'sorry'Real.LIM.abs_eq {a b:ℕ → ℚ} (ha: (a: Sequence).IsCauchy) (hb: (b: Sequence).IsCauchy) (h: LIM a = LIM b): LIM |a| = LIM |b| := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:LIM a = LIM b⊢ LIM |a| = LIM |b| All goals completed! 🐙theorem declaration uses 'sorry'Real.LIM.abs_eq_pos {a: ℕ → ℚ} (h: LIM a > 0) (ha: (a:Sequence).IsCauchy): LIM a = LIM |a| := a:ℕ → ℚh:LIM a > 0ha:(↑a).IsCauchy⊢ LIM a = LIM |a| All goals completed! 🐙theorem declaration uses 'sorry'Real.LIM_abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy): |LIM a| = LIM |a| := a:ℕ → ℚha:(↑a).IsCauchy⊢ |LIM a| = LIM |a| All goals completed! 🐙theorem declaration uses 'sorry'Real.LIM_of_le' {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∃ N, ∀ n ≥ N, a n ≤ x) : LIM a ≤ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∃ N, ∀ n ≥ N, ↑(a n) ≤ x⊢ LIM a ≤ x All goals completed! 🐙

Вправа 5.5.4

theorem declaration uses 'sorry'Real.LIM_of_Cauchy {q:ℕ → ℚ} (hq: ∀ M, ∀ n ≥ M, ∀ n' ≥ M, |q n - q n'| ≤ 1 / (M+1)) : (q:Sequence).IsCauchy ∧ ∀ M, |q M - LIM q| ≤ 1 / (M+1) := q:ℕ → ℚhq:∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)⊢ (↑q).IsCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1) All goals completed! 🐙

Послідовність m₁, m₂, … визначена коректно. Цей доказ використовує іншу угоду щодо індексації, ніж у тексті.

lemma Real.LUB_claim1 (n : ℕ) {E: Set Real} (hE: Set.Nonempty E) (hbound: BddAbove E) : ∃! m:ℤ, (((m:ℚ) / (n+1):ℚ):Real) ∈ upperBounds E ∧ ¬ (((m:ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∈ upperBounds E := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have hpos : ε.IsPos := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))⊢ 0 < ↑n + 1; All goals completed! 🐙 n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:Chapter5.Real.IsPos _fvar.75653 := ?_mvar.75735⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds En:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:Chapter5.Real.IsPos _fvar.75653 := ?_mvar.75735⊢ ∀ (y₁ y₂ : ℤ), ↑(↑y₁ / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑y₁ / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E → ↑(↑y₂ / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑y₂ / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E → y₁ = y₂ n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:Chapter5.Real.IsPos _fvar.75653 := ?_mvar.75735⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyhbound:∃ M, M ∈ upperBounds Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E; n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds E⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝:K > 0hK:↑K * ε > M⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have claim1_1 : L * ε < x₀ := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437⊢ -(↑L' * ε) < x₀; All goals completed! 🐙 have claim1_2 : L * ε ∉ upperBounds E := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E All goals completed! 🐙 have claim1_3 : (K:Real) > (L:Real) := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑K ≤ ↑L⊢ ↑L * ε ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:?_mvar.104281 := Chapter5.Real.mul_le_mul_left _fvar.104277 _fvar.85373⊢ ↑L * ε ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑K * ε ≤ ↑L * ε⊢ ↑L * ε ∈ upperBounds E replace claim1_2 : M ≤ L * ε := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E All goals completed! 🐙 All goals completed! 🐙 have claim1_4 : ∃ m:ℤ, L < m ∧ m ≤ K ∧ m*ε ∈ upperBounds E ∧ (m-1)*ε ∉ upperBounds E := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157⊢ L < ↑Kn:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157⊢ ↑↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157⊢ L < ↑K n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157⊢ ↑L < ↑K; rwa [←gt_iff_lt, gt_of_coen:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157⊢ ↑↑K > ↑↑L n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑_fvar.85437hpos:(↑n + 1)⁻¹.IsPosh✝¹:0 < KhK:M < ↑K * (↑n + 1)⁻¹h✝:0 < L'hL:-x₀ < ↑L' * (↑n + 1)⁻¹claim1_1:↑L * (↑n + 1)⁻¹ < x₀claim1_2:↑L * (↑n + 1)⁻¹ ∉ upperBounds Eclaim1_3:↑L < ↑K⊢ ↑K * (↑n + 1)⁻¹ ∈ upperBounds E; n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑_fvar.85437hpos:(↑n + 1)⁻¹.IsPosh✝¹:0 < KhK:M < ↑K * (↑n + 1)⁻¹h✝:0 < L'hL:-x₀ < ↑L' * (↑n + 1)⁻¹claim1_1:↑L * (↑n + 1)⁻¹ < x₀claim1_2:↑L * (↑n + 1)⁻¹ ∉ upperBounds Eclaim1_3:↑L < ↑K⊢ M ≤ ↑K * (↑n + 1)⁻¹; All goals completed! 🐙 n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E; n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have : (m/(n+1):ℚ) = m*ε := n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := ?_mvar.86354claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := ?_mvar.91571claim1_3:↑_fvar.85410 > ↑_fvar.85489 := ?_mvar.104157m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ↑m / (↑n + 1) = ↑m * (↑n + 1)⁻¹; All goals completed! 🐙 exact ⟨ n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := Eq.mpr (id (congrArg (fun x => x < _fvar.85370) (Eq.trans (congrArg (fun x => x * _fvar.85372) (Eq.trans (Int.cast_neg ↑_fvar.85437) (congrArg Neg.neg (Int.cast_natCast _fvar.85437)))) (neg_mul (↑_fvar.85437) _fvar.85372)))) (lt_of_not_ge 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.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85370 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85370 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85372 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.85449) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := Chapter5.Real.LUB_claim1._proof_2 _fvar.23999 _fvar.24001 _fvar.85371 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355claim1_3:↑_fvar.85410 > ↑_fvar.85489 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85410 ↑_fvar.85489) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85489 * _fvar.85372 ∈ upperBounds _fvar.24000)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85373; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85422 (le_antisymm (le_trans (le_of_lt _fvar.85422) (le_refl (↑_fvar.85410 * _fvar.85372))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85372 ↑_fvar.85410)) (mul_comm _fvar.85372 ↑_fvar.85489)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85403)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.23999 _fvar.24001 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355 claim1_2) _fvar.91572m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147747 / (↑_fvar.23999 + 1)) = ↑_fvar.147747 * _fvar.85372 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147747) (↑_fvar.23999 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147747)) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147747) (Eq.trans (Rat.cast_div 1 (↑_fvar.23999 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))) (one_div (↑_fvar.23999 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147747 / (↑_fvar.23999 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147747) (inv_eq_one_div (↑_fvar.23999 + 1))) (mul_div_assoc' (↑_fvar.147747) 1 (↑_fvar.23999 + 1))) (congrArg (fun x => x / (↑_fvar.23999 + 1)) (mul_one ↑_fvar.147747)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1))))))) (Eq.trans (congrArg (fun x => x = ↑_fvar.147747) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147747) (↑_fvar.23999 + 1) (↑_fvar.23999 + 1)) (mul_div_cancel_right₀ (↑_fvar.147747) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1)))))))) (eq_self ↑_fvar.147747))))⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E All goals completed! 🐙, n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := Eq.mpr (id (congrArg (fun x => x < _fvar.85370) (Eq.trans (congrArg (fun x => x * _fvar.85372) (Eq.trans (Int.cast_neg ↑_fvar.85437) (congrArg Neg.neg (Int.cast_natCast _fvar.85437)))) (neg_mul (↑_fvar.85437) _fvar.85372)))) (lt_of_not_ge 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.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85370 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85370 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85372 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.85449) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := Chapter5.Real.LUB_claim1._proof_2 _fvar.23999 _fvar.24001 _fvar.85371 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355claim1_3:↑_fvar.85410 > ↑_fvar.85489 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85410 ↑_fvar.85489) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85489 * _fvar.85372 ∈ upperBounds _fvar.24000)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85373; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85422 (le_antisymm (le_trans (le_of_lt _fvar.85422) (le_refl (↑_fvar.85410 * _fvar.85372))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85372 ↑_fvar.85410)) (mul_comm _fvar.85372 ↑_fvar.85489)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85403)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.23999 _fvar.24001 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355 claim1_2) _fvar.91572m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147747 / (↑_fvar.23999 + 1)) = ↑_fvar.147747 * _fvar.85372 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147747) (↑_fvar.23999 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147747)) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147747) (Eq.trans (Rat.cast_div 1 (↑_fvar.23999 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))) (one_div (↑_fvar.23999 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147747 / (↑_fvar.23999 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147747) (inv_eq_one_div (↑_fvar.23999 + 1))) (mul_div_assoc' (↑_fvar.147747) 1 (↑_fvar.23999 + 1))) (congrArg (fun x => x / (↑_fvar.23999 + 1)) (mul_one ↑_fvar.147747)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1))))))) (Eq.trans (congrArg (fun x => x = ↑_fvar.147747) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147747) (↑_fvar.23999 + 1) (↑_fvar.23999 + 1)) (mul_div_cancel_right₀ (↑_fvar.147747) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1)))))))) (eq_self ↑_fvar.147747))))⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24001hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.23999 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85437claim1_1:↑_fvar.85489 * _fvar.85372 < _fvar.85370 := Eq.mpr (id (congrArg (fun x => x < _fvar.85370) (Eq.trans (congrArg (fun x => x * _fvar.85372) (Eq.trans (Int.cast_neg ↑_fvar.85437) (congrArg Neg.neg (Int.cast_natCast _fvar.85437)))) (neg_mul (↑_fvar.85437) _fvar.85372)))) (lt_of_not_ge 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.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85370 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85370) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85437) (Mathlib.Tactic.Ring.atom_pf _fvar.85372) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85372 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85437 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85372 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.85370 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85437 ^ Nat.rawCast 1 * (_fvar.85372 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85370 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.85437) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85372 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.85449) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85489 * _fvar.85372 ∉ upperBounds _fvar.24000 := Chapter5.Real.LUB_claim1._proof_2 _fvar.23999 _fvar.24001 _fvar.85371 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355claim1_3:↑_fvar.85410 > ↑_fvar.85489 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85410 ↑_fvar.85489) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85489 * _fvar.85372 ∈ upperBounds _fvar.24000)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85373; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85422 (le_antisymm (le_trans (le_of_lt _fvar.85422) (le_refl (↑_fvar.85410 * _fvar.85372))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85372 ↑_fvar.85410)) (mul_comm _fvar.85372 ↑_fvar.85489)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85403)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.23999 _fvar.24001 _fvar.85373 _fvar.85403 _fvar.85404 _fvar.85410 _fvar.85418 _fvar.85422 _fvar.85437 _fvar.85445 _fvar.85449 _fvar.86355 claim1_2) _fvar.91572m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147747 / (↑_fvar.23999 + 1)) = ↑_fvar.147747 * _fvar.85372 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147747) (↑_fvar.23999 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147747)) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147747) (Eq.trans (Rat.cast_div 1 (↑_fvar.23999 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.23999) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.23999)) Rat.cast_one))) (one_div (↑_fvar.23999 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147747 / (↑_fvar.23999 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147747) (inv_eq_one_div (↑_fvar.23999 + 1))) (mul_div_assoc' (↑_fvar.147747) 1 (↑_fvar.23999 + 1))) (congrArg (fun x => x / (↑_fvar.23999 + 1)) (mul_one ↑_fvar.147747)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1))))))) (Eq.trans (congrArg (fun x => x = ↑_fvar.147747) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147747) (↑_fvar.23999 + 1) (↑_fvar.23999 + 1)) (mul_div_cancel_right₀ (↑_fvar.147747) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.23999) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one) (Eq.refl (Nat.ble 1 1)))))))) (eq_self ↑_fvar.147747))))⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) = (↑m - 1) * ε; All goals completed! 🐙 ⟩ All goals completed! 🐙
lemma Real.LUB_claim2 {E : Set Real} (N:ℕ) {a b: ℕ → ℚ} (hb : ∀ n, b n = 1 / (↑n + 1)) (hm1 : ∀ (n : ℕ), ↑(a n) ∈ upperBounds E) (hm2 : ∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E) : ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (N+1) := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ |a n - a n'| ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n' ∧ a n - a n' ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n'E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ a n - a n' ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n' E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds E⊢ -(1 / (↑N + 1)) ≤ a n - a n'; E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds E⊢ -(1 / (↑N + 1)) ≤ a n - a n' have bound1 : ((a-b) n') < a n := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds E⊢ ↑((a - b) n') < ↑(a n); E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑(a n) ≤ ↑((a - b) n')⊢ ↑((a - b) n') ∈ upperBounds E; All goals completed! 🐙 have bound3 : 1/((n':ℚ)+1) ≤ 1/(N+1) := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) All goals completed! 🐙 E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds Ebound1:@HSub.hSub ?_mvar.191137 ?_mvar.191138 ?_mvar.191139 ?_mvar.191140 _fvar.190509 _fvar.190510 _fvar.190523 < @_fvar.190509 _fvar.190517 := ?_mvar.191184bound3:-(1 / (↑N + 1)) ≤ -(1 / (↑n' + 1))⊢ -(1 / (↑N + 1)) ≤ a n - a n'; E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds Ebound1:a n' - b n' < a nbound3:-(1 / (↑N + 1)) ≤ -(1 / (↑n' + 1))⊢ -(1 / (↑N + 1)) ≤ a n - a n'; All goals completed! 🐙 E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds En:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds E⊢ a n - a n' ≤ 1 / (↑N + 1); E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds E⊢ a n - a n' ≤ 1 / (↑N + 1) have bound1 : ((a-b) n) < a n' := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds E⊢ ↑((a - b) n) < ↑(a n'); E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)n:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑(a n') ≤ ↑((a - b) n)⊢ ↑((a - b) n) ∈ upperBounds E; All goals completed! 🐙 have bound2 : ((a-b) n) = a n - 1 / (n+1) := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) All goals completed! 🐙 have bound3 : 1/((n+1):ℚ) ≤ 1/(N+1) := E:Set RealN:ℕa:ℕ → ℚb:ℕ → ℚhb:∀ (n : ℕ), b n = 1 / (↑n + 1)hm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) All goals completed! 🐙 All goals completed! 🐙

Теорема 5.5.9 (Існування найменшої верхньої межі)

theorem Real.LUB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddAbove E): ∃ S, IsLUB E S := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choose⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).left⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).right⊢ ∃ S, IsLUB E S have claim2 (N:ℕ) := LUB_claim2 N (E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := @Set.Nonempty.some_mem Chapter5.Real _fvar.227760 _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightN:ℕ⊢ ∀ (n : ℕ), b n = 1 / (↑n + 1) All goals completed! 🐙) hm1 hm2 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).left⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262⊢ ∃ S, IsLUB E S; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262⊢ IsLUB E S have claim4 : S = LIM (a - b) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262this:Chapter5.LIM _fvar.228513 = 0 := Chapter5.Real.LIM.harmonic⊢ S = LIM (a - b) All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687⊢ (∀ x ∈ E, x ≤ S) ∧ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687⊢ ∀ x ∈ E, x ≤ SE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687⊢ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687⊢ ∀ x ∈ E, x ≤ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687x✝:Reala✝:x✝ ∈ E⊢ x✝ ≤ S; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687x✝:Reala✝:x✝ ∈ E⊢ ∀ (n : ℕ), ↑(a n) ≥ x✝; All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds E⊢ y ≥ S have claim5 (n:ℕ) : y ≥ (a-b) n := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).leftclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ∃ n, ↑((a - b) n) ∈ upperBounds E; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).leftclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ↑((a - b) n) ∈ upperBounds E; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).leftclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ y ≤ ↑((a - b) n); All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), _fvar.262504 ≥ ↑((_fvar.228262 - _fvar.228513) n) := fun n => @?_mvar.262683 n⊢ y ≥ LIM (a - b); E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227761hx₀:_fvar.227775 ∈ _fvar.227760 := Set.Nonempty.some_mem _fvar.227761m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.227958 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227760 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227760 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227761 _fvar.227762hb:(↑_fvar.228513).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228262 - _fvar.228513) n) ∉ upperBounds _fvar.227760 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228614 n))).rightclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1) := fun N => Chapter5.Real.LUB_claim2 N (@?_mvar.229126 N) _fvar.228814 _fvar.229066claim3:(↑_fvar.228262).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229127).leftS:Chapter5.Real := Chapter5.LIM _fvar.228262claim4:_fvar.245397 = Chapter5.LIM (_fvar.228262 - _fvar.228513) := ?_mvar.245687y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), _fvar.262504 ≥ ↑((_fvar.228262 - _fvar.228513) n) := fun n => @?_mvar.262683 n⊢ (↑(a - b)).IsCauchy; All goals completed! 🐙

Простий розширений клас дійсної величини для визначення супремуму.

inductive ExtendedReal where | neg_infty : ExtendedReal | real (x:Real) : ExtendedReal | infty : ExtendedReal

Mathlib надає перевагу ⊤ для позначення елемента +∞.

instance ExtendedReal.inst_Top : Top ExtendedReal where top := infty

Mathlib надає перевагу ⊥ для позначення елемента -∞.

instance ExtendedReal.inst_Bot: Bot ExtendedReal where bot := neg_infty
instance ExtendedReal.coe_real : Coe Real ExtendedReal where coe x := ExtendedReal.real xinstance ExtendedReal.real_coe : Coe ExtendedReal Real where coe X := match X with | neg_infty => 0 | real x => x | infty => 0abbrev ExtendedReal.IsFinite (X : ExtendedReal) : Prop := match X with | neg_infty => False | real _ => True | infty => Falsetheorem ExtendedReal.finite_eq_coe {X: ExtendedReal} (hX: X.IsFinite) : X = ((X:Real):ExtendedReal) := X:ExtendedRealhX:X.IsFinite⊢ X = real (match X with | neg_infty => 0 | real x => x | infty => 0) hX:neg_infty.IsFinite⊢ neg_infty = real (match neg_infty with | neg_infty => 0 | real x => x | infty => 0)x✝:RealhX:(real x✝).IsFinite⊢ real x✝ = real (match real x✝ with | neg_infty => 0 | real x => x | infty => 0)hX:infty.IsFinite⊢ infty = real (match infty with | neg_infty => 0 | real x => x | infty => 0) hX:neg_infty.IsFinite⊢ neg_infty = real (match neg_infty with | neg_infty => 0 | real x => x | infty => 0)x✝:RealhX:(real x✝).IsFinite⊢ real x✝ = real (match real x✝ with | neg_infty => 0 | real x => x | infty => 0)hX:infty.IsFinite⊢ infty = real (match infty with | neg_infty => 0 | real x => x | infty => 0) try All goals completed! 🐙 All goals completed! 🐙open Classical in /-- Визначення 5.5.10 (Супремум)-/ noncomputable abbrev ExtendedReal.sup (E: Set Real) : ExtendedReal := if h1:E.Nonempty then (if h2:BddAbove E then ((Real.LUB_exist h1 h2).choose:Real) else ⊤) else ⊥

Визначення 5.5.10 (Супремум)

theorem ExtendedReal.sup_of_empty : sup ∅ = ⊥ := ⊢ sup ∅ = ⊥ All goals completed! 🐙

Визначення 5.5.10 (Супремум)

theorem ExtendedReal.sup_of_unbounded {E: Set Real} (hb: ¬ BddAbove E) : sup E = ⊤ := E:Set Realhb:¬BddAbove E⊢ sup E = ⊤ have hE : E.Nonempty := E:Set Realhb:¬BddAbove E⊢ sup E = ⊤ E:Set Realhb:E = ∅⊢ BddAbove E; All goals completed! 🐙 All goals completed! 🐙

Визначення 5.5.10 (Супремум)

theorem ExtendedReal.sup_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : IsLUB E (sup E) := E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E (match sup E with | neg_infty => 0 | real x => x | infty => 0) E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E ⋯.choose; All goals completed! 🐙
theorem ExtendedReal.sup_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : (sup E).IsFinite := E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ (sup E).IsFinite All goals completed! 🐙

Твердження 5.5.12

theorem declaration uses 'sorry'Real.exist_sqrt_two : ∃ x:Real, x^2 = 2 := ⊢ ∃ x, x ^ 2 = 2 -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∃ x, x ^ 2 = 2 have claim1: 2 ∈ upperBounds E := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∀ x ∈ E, x ≤ 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:y ∈ E⊢ y ≤ 2; E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:0 ≤ y ∧ y ^ 2 < 2⊢ y ≤ 2; E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < y⊢ 0 ≤ y → 2 ≤ y ^ 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ y ^ 2 calc _ ≤ 2 * 2 := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ 2 * 2 All goals completed! 🐙 _ ≤ y * y := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 * 2 ≤ y * y All goals completed! 🐙 _ = y^2 := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ y * y = y ^ 2 All goals completed! 🐙 have claim1' : BddAbove E := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512⊢ ∃ M, M ∈ upperBounds E; All goals completed! 🐙 have claim2: 1 ∈ E := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonempty⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0⊢ ∃ x, x ^ 2 = 2 have claim3 : IsLUB E x := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have claim4 : x ≥ 1 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have claim5 : x ≤ 2 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have claim6 : x.IsPos := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096⊢ x > 0; All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645⊢ x ^ 2 = 2; E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2⊢ x ^ 2 = 2E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2⊢ x ^ 2 = 2E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 = 2⊢ x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2⊢ x ^ 2 = 2 have claim11: ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 - 4*ε > 2 := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 have hx : x^2 - 2 > 0 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have hε : 0 < ε := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ x ^ 2 - 4 * ε > 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301506 ^ 2 - 2) / 8)hx:_fvar.301506 ^ 2 - 2 > 0 := ?_mvar.324201hε:0 < _fvar.323757 := ?_mvar.324488hε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ x ^ 2 - 4 * ε > 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 = 2 have claim12: (x-ε)^2 > 2 := calc _ = x^2 - 2 * ε * x + ε * ε := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ (x - ε) ^ 2 = x ^ 2 - 2 * ε * x + ε * ε All goals completed! 🐙 _ ≥ x^2 - 2 * ε * 2 + 0 * 0 := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * x + ε * ε ≥ x ^ 2 - 2 * ε * 2 + 0 * 0 All goals completed! 🐙 _ = x^2 - 4 * ε := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * 2 + 0 * 0 = x ^ 2 - 4 * ε All goals completed! 🐙 _ > 2 := hε3 have why (y:Real) (hy: y ∈ E) : x - ε ≥ y := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have claim13: x-ε ∈ upperBounds E := ⊢ ∃ x, x ^ 2 = 2 rwa [upperBound_defE:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2claim12:(_fvar.301506 - _fvar.472342) ^ 2 > 2 := Trans.trans (Trans.trans (Trans.trans ?_mvar.473091 ?_mvar.473458) ?_mvar.474001) _fvar.472364why:∀ y ∈ _fvar.284319, _fvar.301506 - _fvar.472342 ≥ y := fun y hy => @?_mvar.500906 y hy⊢ ∀ x_1 ∈ E, x_1 ≤ x - ε have claim14: x ≤ x-ε := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2⊢ x ^ 2 = 2 have claim7 : ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 + 5*ε < 2 := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 have hx : 2 - x^2 > 0 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have hε: 0 < ε := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917hε2:_fvar.521661 ≤ (2 - _fvar.301506 ^ 2) / 10 := min_le_right ?_mvar.526350 ?_mvar.526351⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917hε2:_fvar.521661 ≤ (2 - _fvar.301506 ^ 2) / 10 := min_le_right ?_mvar.526350 ?_mvar.526351⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917hε2:_fvar.521661 ≤ (2 - _fvar.301506 ^ 2) / 10 := min_le_right ?_mvar.526350 ?_mvar.526351⊢ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917hε2:_fvar.521661 ≤ (2 - _fvar.301506 ^ 2) / 10 := min_le_right ?_mvar.526350 ?_mvar.526351⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301506 ^ 2) / 10)hx:2 - _fvar.301506 ^ 2 > 0 := ?_mvar.522105hε:0 < _fvar.521661 := ?_mvar.522395hε1:_fvar.521661 ≤ 1 / 2 := min_le_left ?_mvar.525916 ?_mvar.525917hε2:_fvar.521661 ≤ (2 - _fvar.301506 ^ 2) / 10 := min_le_right ?_mvar.526350 ?_mvar.526351⊢ x ^ 2 + 5 * ε < 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 = 2 have claim8 : (x+ε)^2 < 2 := calc _ = x^2 + (2*x)*ε + ε*ε := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ (x + ε) ^ 2 = x ^ 2 + 2 * x * ε + ε * ε All goals completed! 🐙 _ ≤ x^2 + (2*2)*ε + 1*ε := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * x * ε + ε * ε ≤ x ^ 2 + 2 * 2 * ε + 1 * ε All goals completed! 🐙 _ = x^2 + 5*ε := E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284319 2)))) fun y hy => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_le_eq y 2) (Eq.trans (Mathlib.Tactic.PushNeg.not_and_eq (0 ≤ y) (y ^ 2 < 2)) (implies_congr (Eq.refl (0 ≤ y)) (Mathlib.Tactic.PushNeg.not_lt_eq (y ^ 2) 2))))) fun hy hpos => Trans.trans (Trans.trans (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl 4)) (Eq.refl true)) (mul_le_mul (le_of_lt hy) (le_of_lt hy) (le_of_lt (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))) (le_of_lt (lt_trans (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) hy)))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap y (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.atom_pf y) (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 (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 2) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))))) (Eq.mp (congrArg (fun x => y ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) hy)claim1':BddAbove _fvar.284319 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284319)))) (Exists.intro 2 _fvar.284513)claim2:1 ∈ _fvar.284319 := of_eq_true (Eq.trans (congrArg (fun x => 1 ∈ setOf x) (funext fun y => congrArg (fun x => x ∧ y ^ 2 < 2) ge_iff_le._simp_1)) (Eq.trans (congr (congrArg And zero_le_one._simp_1) (Eq.trans (congrArg (fun x => x < 2) (one_pow 2)) Nat.one_lt_ofNat._simp_1)) (and_self True)))claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.294982 _fvar.301418claim4:_fvar.301506 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295130 _fvar.301818claim5:_fvar.301506 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284513 _fvar.301818claim6:Chapter5.Real.IsPos _fvar.301506 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301506)))) (lt_of_not_ge 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.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_one)) (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301506 (Nat.rawCast 1) (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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 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_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).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 Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.301506 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301506) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.301506 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301506 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw Chapter5.Real (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw Chapter5.Real 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Chapter5.Real Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.307943)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * 2 * ε + 1 * ε = x ^ 2 + 5 * ε All goals completed! 🐙 _ < 2 := hε3 have claim9 : x + ε ∈ E := ⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284319 := ?_mvar.284512claim1':BddAbove _fvar.284319 := ?_mvar.294981claim2:1 ∈ _fvar.284319 := ?_mvar.295129claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284319 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284319 _fvar.301506 := ?_mvar.301817claim4:_fvar.301506 ≥ 1 := ?_mvar.307942claim5:_fvar.301506 ≤ 2 := ?_mvar.314096claim6:Chapter5.Real.IsPos _fvar.301506 := ?_mvar.319645h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(_fvar.301506 + _fvar.535552) ^ 2 < 2 := Trans.trans (Trans.trans (Trans.trans ?_mvar.536256 ?_mvar.536604) ?_mvar.537122) _fvar.535574⊢ 0 ≤ x + ε; All goals completed! 🐙 have claim10 : x + ε ≤ x := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙

Ремарка 5.5.13

theorem declaration uses 'sorry'Real.exist_irrational : ∃ x:Real, ¬ ∃ q:ℚ, x = (q:Real) := ⊢ ∃ x, ¬∃ q, x = ↑q All goals completed! 🐙

Допоміжна лема для Вправи 5.5.1.

theorem Real.mem_neg (E: Set Real) (x:Real) : x ∈ -E ↔ -x ∈ E := Set.mem_neg

Вправа 5.5.1

theorem declaration uses 'sorry'Real.inf_neg {E: Set Real} {M:Real} (h: IsLUB E M) : IsGLB (-E) (-M) := E:Set RealM:Realh:IsLUB E M⊢ IsGLB (-E) (-M) All goals completed! 🐙
theorem declaration uses 'sorry'Real.GLB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddBelow E): ∃ S, IsGLB E S := E:Set RealhE:E.Nonemptyhbound:BddBelow E⊢ ∃ S, IsGLB E S All goals completed! 🐙open Classical in noncomputable abbrev ExtendedReal.inf (E: Set Real) : ExtendedReal := if h1:E.Nonempty then (if h2:BddBelow E then ((Real.GLB_exist h1 h2).choose:Real) else ⊥) else ⊤theorem ExtendedReal.inf_of_empty : inf ∅ = ⊤ := ⊢ inf ∅ = ⊤ All goals completed! 🐙theorem ExtendedReal.inf_of_unbounded {E: Set Real} (hb: ¬ BddBelow E) : inf E = ⊥ := E:Set Realhb:¬BddBelow E⊢ inf E = ⊥ have hE : E.Nonempty := E:Set Realhb:¬BddBelow E⊢ inf E = ⊥ E:Set Realhb:E = ∅⊢ BddBelow E; All goals completed! 🐙 All goals completed! 🐙theorem ExtendedReal.inf_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) : IsGLB E (inf E) := E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E (match inf E with | neg_infty => 0 | real x => x | infty => 0) E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E ⋯.choose; All goals completed! 🐙theorem ExtendedReal.inf_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) : (inf E).IsFinite := E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ (inf E).IsFinite All goals completed! 🐙

Вправа 5.5.5

theorem declaration uses 'sorry'Real.irrat_between {x y:Real} (hxy: x < y) : ∃ z, x < z ∧ z < y ∧ ¬ ∃ q:ℚ, z = (q:Real) := x:Realy:Realhxy:x < y⊢ ∃ z, x < z ∧ z < y ∧ ¬∃ q, z = ↑q All goals completed! 🐙
/- Використайте поняття супремуму в цьому розділі для визначення операції `sSup` в Mathlib -/ noncomputable instance Real.inst_SupSet : SupSet Real where sSup E := ((ExtendedReal.sup E):Real)

Використайте операцію SupSet.sSup.{u_1} {α : Type u_1} [self : SupSet α] : Set α → αsSup для побудови умовно повної ґратчастої структури на Chapter5.Real : TypeReal

noncomputable instance Real.inst_conditionallyCompleteLattice : ConditionallyCompleteLattice Real := conditionallyCompleteLatticeOfLatticeOfsSup Real (⊢ ∀ (s : Set Real), BddAbove s → s.Nonempty → IsLUB s (sSup s) s✝:Set Reala✝¹:BddAbove s✝a✝:s✝.Nonempty⊢ IsLUB s✝ (sSup s✝); All goals completed! 🐙)
theorem ExtendedReal.sSup_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : IsLUB E (sSup E) := sup_of_bounded hnon hbend Chapter5