The least upper bound property

Analysis I, Section 5.5: The least upper bound property

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

Main constructions and results of this section:

  • Upper bound and least upper bound on the real line

Tips from past users

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

  • (Add tip here)

namespace Chapter5

Definition 5.5.1 (upper bounds). Here we use the upperBounds.{u_1} {α : Type u_1} [LE α] (s : Set α) : Set αupperBounds set defined in 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 for Example 5.5.2

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

API for Example 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! 🐙

Example 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 for Example 5.5.3

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

Example 5.5.3

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

Example 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! 🐙

Definition 5.5.5 (least upper bound). Here we use the Unknown identifier `isLUB`isLUB predicate defined in 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! 🐙

Example 5.5.6

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

Example 5.5.7

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

Proposition 5.5.8 (Uniqueness of least upper bound)

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! 🐙

definition of "bounded above", using Mathlib notation

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

Exercise 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! 🐙

Exercise 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! 🐙

Lemmas that can be helpful for proving 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! 🐙

Exercise 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! 🐙

The sequence m₁, m₂, … is well-defined. This proof uses a different indexing convention than the text

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.24206⊢ ∃! 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.24206hx₀: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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))⊢ 0 < ↑n + 1; All goals completed! 🐙 n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:Chapter5.Real.IsPos _fvar.75858 := ?_mvar.75940⊢ ∃ 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:Chapter5.Real.IsPos _fvar.75858 := ?_mvar.75940⊢ ∀ (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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:Chapter5.Real.IsPos _fvar.75858 := ?_mvar.75940⊢ ∃ 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642⊢ ∃ 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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642⊢ -(↑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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑K ≤ ↑L⊢ ↑L * ε ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:?_mvar.104486 := Chapter5.Real.mul_le_mul_left _fvar.104482 _fvar.85578⊢ ↑L * ε ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362⊢ L < ↑Kn:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362⊢ ↑↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362⊢ L < ↑K n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362⊢ ↑L < ↑K; rwa [←gt_iff_lt, gt_of_coen:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362⊢ ↑↑K > ↑↑L n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑_fvar.85642hpos:(↑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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑_fvar.85642hpos:(↑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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362m:ℤ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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362m:ℤ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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := ?_mvar.86559claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := ?_mvar.91776claim1_3:↑_fvar.85615 > ↑_fvar.85694 := ?_mvar.104362m:ℤ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.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := Eq.mpr (id (congrArg (fun x => x < _fvar.85575) (Eq.trans (congrArg (fun x => x * _fvar.85577) (Eq.trans (Int.cast_neg ↑_fvar.85642) (congrArg Neg.neg (Int.cast_natCast _fvar.85642)))) (neg_mul (↑_fvar.85642) _fvar.85577)))) (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.85575) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85575 (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.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85575) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85575 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85577 (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.85654) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := Chapter5.Real.LUB_claim1._proof_2 _fvar.24204 _fvar.24206 _fvar.85576 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560claim1_3:↑_fvar.85615 > ↑_fvar.85694 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85615 ↑_fvar.85694) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85694 * _fvar.85577 ∈ upperBounds _fvar.24205)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85578; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85627 (le_antisymm (le_trans (le_of_lt _fvar.85627) (le_refl (↑_fvar.85615 * _fvar.85577))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85577 ↑_fvar.85615)) (mul_comm _fvar.85577 ↑_fvar.85694)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85608)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.24204 _fvar.24206 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560 claim1_2) _fvar.91777m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147952 / (↑_fvar.24204 + 1)) = ↑_fvar.147952 * _fvar.85577 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147952) (↑_fvar.24204 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147952)) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147952) (Eq.trans (Rat.cast_div 1 (↑_fvar.24204 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))) (one_div (↑_fvar.24204 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147952 / (↑_fvar.24204 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147952) (inv_eq_one_div (↑_fvar.24204 + 1))) (mul_div_assoc' (↑_fvar.147952) 1 (↑_fvar.24204 + 1))) (congrArg (fun x => x / (↑_fvar.24204 + 1)) (mul_one ↑_fvar.147952)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147952) (↑_fvar.24204 + 1) (↑_fvar.24204 + 1)) (mul_div_cancel_right₀ (↑_fvar.147952) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952))))⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E All goals completed! 🐙, n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := Eq.mpr (id (congrArg (fun x => x < _fvar.85575) (Eq.trans (congrArg (fun x => x * _fvar.85577) (Eq.trans (Int.cast_neg ↑_fvar.85642) (congrArg Neg.neg (Int.cast_natCast _fvar.85642)))) (neg_mul (↑_fvar.85642) _fvar.85577)))) (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.85575) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85575 (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.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85575) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85575 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85577 (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.85654) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := Chapter5.Real.LUB_claim1._proof_2 _fvar.24204 _fvar.24206 _fvar.85576 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560claim1_3:↑_fvar.85615 > ↑_fvar.85694 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85615 ↑_fvar.85694) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85694 * _fvar.85577 ∈ upperBounds _fvar.24205)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85578; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85627 (le_antisymm (le_trans (le_of_lt _fvar.85627) (le_refl (↑_fvar.85615 * _fvar.85577))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85577 ↑_fvar.85615)) (mul_comm _fvar.85577 ↑_fvar.85694)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85608)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.24204 _fvar.24206 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560 claim1_2) _fvar.91777m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147952 / (↑_fvar.24204 + 1)) = ↑_fvar.147952 * _fvar.85577 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147952) (↑_fvar.24204 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147952)) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147952) (Eq.trans (Rat.cast_div 1 (↑_fvar.24204 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))) (one_div (↑_fvar.24204 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147952 / (↑_fvar.24204 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147952) (inv_eq_one_div (↑_fvar.24204 + 1))) (mul_div_assoc' (↑_fvar.147952) 1 (↑_fvar.24204 + 1))) (congrArg (fun x => x / (↑_fvar.24204 + 1)) (mul_one ↑_fvar.147952)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147952) (↑_fvar.24204 + 1) (↑_fvar.24204 + 1)) (mul_div_cancel_right₀ (↑_fvar.147952) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952))))⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E n:ℕE:Set RealhE:E.Nonemptyx₀:Chapter5.Real := Set.Nonempty.some _fvar.24206hx₀:hE.some ∈ Eε:Chapter5.Real := ↑(1 / (↑_fvar.24204 + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑_fvar.85642claim1_1:↑_fvar.85694 * _fvar.85577 < _fvar.85575 := Eq.mpr (id (congrArg (fun x => x < _fvar.85575) (Eq.trans (congrArg (fun x => x * _fvar.85577) (Eq.trans (Int.cast_neg ↑_fvar.85642) (congrArg Neg.neg (Int.cast_natCast _fvar.85642)))) (neg_mul (↑_fvar.85642) _fvar.85577)))) (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.85575) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.85575 (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.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.85575) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.85642) (Mathlib.Tactic.Ring.atom_pf _fvar.85577) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right _fvar.85577 (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (↑_fvar.85642 ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_mul _fvar.85577 (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.85575 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑_fvar.85642 ^ Nat.rawCast 1 * (_fvar.85577 ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85575 (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.85642) (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.85577 (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.85654) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))))claim1_2:↑_fvar.85694 * _fvar.85577 ∉ upperBounds _fvar.24205 := Chapter5.Real.LUB_claim1._proof_2 _fvar.24204 _fvar.24206 _fvar.85576 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560claim1_3:↑_fvar.85615 > ↑_fvar.85694 := Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_gt_eq ↑_fvar.85615 ↑_fvar.85694) (Mathlib.Tactic.PushNeg.not_not_eq (↑_fvar.85694 * _fvar.85577 ∈ upperBounds _fvar.24205)))) fun claim1_2 => have claim1_2 := Chapter5.Real.mul_le_mul_left claim1_2 _fvar.85578; have claim1_2 := Decidable.byContradiction fun a => ne_of_lt _fvar.85627 (le_antisymm (le_trans (le_of_lt _fvar.85627) (le_refl (↑_fvar.85615 * _fvar.85577))) (le_trans (Eq.mp (congr (congrArg LE.le (mul_comm _fvar.85577 ↑_fvar.85615)) (mul_comm _fvar.85577 ↑_fvar.85694)) claim1_2) (le_trans (le_of_not_ge a) (le_refl _fvar.85608)))); Chapter5.Real.LUB_claim1._proof_3 _fvar.24204 _fvar.24206 _fvar.85578 _fvar.85608 _fvar.85609 _fvar.85615 _fvar.85623 _fvar.85627 _fvar.85642 _fvar.85650 _fvar.85654 _fvar.86560 claim1_2) _fvar.91777m:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑_fvar.147952 / (↑_fvar.24204 + 1)) = ↑_fvar.147952 * _fvar.85577 := Eq.mpr (id (congr (congrArg Eq (Eq.trans (Rat.cast_div (↑_fvar.147952) (↑_fvar.24204 + 1)) (congr (congrArg HDiv.hDiv (Rat.cast_intCast _fvar.147952)) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))))) (congrArg (HMul.hMul ↑_fvar.147952) (Eq.trans (Rat.cast_div 1 (↑_fvar.24204 + 1)) (Eq.trans (congr (congrArg HDiv.hDiv Rat.cast_one) (Eq.trans (Rat.cast_add (↑_fvar.24204) 1) (congr (congrArg HAdd.hAdd (Rat.cast_natCast _fvar.24204)) Rat.cast_one))) (one_div (↑_fvar.24204 + 1))))))) (of_eq_true (Eq.trans (Eq.trans (congrArg (Eq (↑_fvar.147952 / (↑_fvar.24204 + 1))) (Eq.trans (Eq.trans (congrArg (HMul.hMul ↑_fvar.147952) (inv_eq_one_div (↑_fvar.24204 + 1))) (mul_div_assoc' (↑_fvar.147952) 1 (↑_fvar.24204 + 1))) (congrArg (fun x => x / (↑_fvar.24204 + 1)) (mul_one ↑_fvar.147952)))) (eq_div_iff._simp_1 (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952) (Eq.trans (div_mul_eq_mul_div (↑_fvar.147952) (↑_fvar.24204 + 1) (↑_fvar.24204 + 1)) (mul_div_cancel_right₀ (↑_fvar.147952) (ne_of_gt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' _fvar.24204) (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.147952))))⊢ ↑(↑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.191342 ?_mvar.191343 ?_mvar.191344 ?_mvar.191345 _fvar.190714 _fvar.190715 _fvar.190728 < @_fvar.190714 _fvar.190722 := ?_mvar.191389bound3:-(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! 🐙

Theorem 5.5.9 (Existence of least upper bound)

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 -- This proof is written to follow the structure of the original text. E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choose⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).left⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := @Set.Nonempty.some_mem Chapter5.Real _fvar.227965 _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).left⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467⊢ ∃ S, IsLUB E S; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467⊢ 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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467this:Chapter5.LIM _fvar.228718 = 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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892⊢ (∀ x ∈ E, x ≤ S) ∧ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892⊢ ∀ x ∈ E, x ≤ SE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892⊢ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892⊢ ∀ x ∈ E, x ≤ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892x✝:Reala✝:x✝ ∈ E⊢ x✝ ≤ S; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892x✝:Reala✝:x✝ ∈ E⊢ ∀ (n : ℕ), ↑(a n) ≥ x✝; All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y: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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y: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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y: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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y: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.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), _fvar.262709 ≥ ↑((_fvar.228467 - _fvar.228718) n) := fun n => @?_mvar.262888 n⊢ y ≥ LIM (a - b); E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Chapter5.Real := Set.Nonempty.some _fvar.227966hx₀:_fvar.227980 ∈ _fvar.227965 := Set.Nonempty.some_mem _fvar.227966m:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(@_fvar.228163 n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds _fvar.227965 ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds _fvar.227965 := fun n => Chapter5.Real.LUB_claim1 n _fvar.227966 _fvar.227967hb:(↑_fvar.228718).IsCauchy := Chapter5.Sequence.IsCauchy.harmonic'hm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 n))).lefthm2:∀ (n : ℕ), ↑((_fvar.228467 - _fvar.228718) n) ∉ upperBounds _fvar.227965 := fun n => (Exists.choose_spec (ExistsUnique.exists (@_fvar.228819 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.229331 N) _fvar.229019 _fvar.229271claim3:(↑_fvar.228467).IsCauchy := (Chapter5.Real.LIM_of_Cauchy _fvar.229332).leftS:Chapter5.Real := Chapter5.LIM _fvar.228467claim4:_fvar.245602 = Chapter5.LIM (_fvar.228467 - _fvar.228718) := ?_mvar.245892y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), _fvar.262709 ≥ ↑((_fvar.228467 - _fvar.228718) n) := fun n => @?_mvar.262888 n⊢ (↑(a - b)).IsCauchy; All goals completed! 🐙

A bare-bones extended real class to define supremum.

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

Mathlib prefers ⊤ to denote the +∞ element.

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

Mathlib prefers ⊥ to denote the -∞ element.

instance ExtendedReal.inst_Bot: Bot ExtendedReal where bot := 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 /-- Definition 5.5.10 (Supremum)-/ 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 ⊥

Definition 5.5.10 (Supremum)

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

Definition 5.5.10 (Supremum)

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! 🐙

Definition 5.5.10 (Supremum)

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! 🐙

Proposition 5.5.12

theorem declaration uses 'sorry'Real.exist_sqrt_two : ∃ x:Real, x^2 = 2 := ⊢ ∃ x, x ^ 2 = 2 -- This proof is written to follow the structure of the original text. 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.284524 := ?_mvar.284717⊢ ∃ 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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonempty⊢ ∃ x, x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301⊢ x > 0; All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850⊢ x ^ 2 = 2; E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2⊢ x ^ 2 = 2E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2⊢ x ^ 2 = 2E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 = 2⊢ x ^ 2 = 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h: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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Chapter5.Real := min (1 / 2) ((_fvar.301711 ^ 2 - 2) / 8)hx:_fvar.301711 ^ 2 - 2 > 0 := ?_mvar.324406hε:0 < _fvar.323962 := ?_mvar.324693hε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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h: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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2claim12:(_fvar.301711 - _fvar.472547) ^ 2 > 2 := Trans.trans (Trans.trans (Trans.trans ?_mvar.473296 ?_mvar.473663) ?_mvar.474206) _fvar.472569why:∀ y ∈ _fvar.284524, _fvar.301711 - _fvar.472547 ≥ y := fun y hy => @?_mvar.501111 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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h: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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122hε2:_fvar.521866 ≤ (2 - _fvar.301711 ^ 2) / 10 := min_le_right ?_mvar.526555 ?_mvar.526556⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122hε2:_fvar.521866 ≤ (2 - _fvar.301711 ^ 2) / 10 := min_le_right ?_mvar.526555 ?_mvar.526556⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122hε2:_fvar.521866 ≤ (2 - _fvar.301711 ^ 2) / 10 := min_le_right ?_mvar.526555 ?_mvar.526556⊢ x ^ 2 + 5 * ε < 2 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122hε2:_fvar.521866 ≤ (2 - _fvar.301711 ^ 2) / 10 := min_le_right ?_mvar.526555 ?_mvar.526556⊢ ε < 1E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Chapter5.Real := min (1 / 2) ((2 - _fvar.301711 ^ 2) / 10)hx:2 - _fvar.301711 ^ 2 > 0 := ?_mvar.522310hε:0 < _fvar.521866 := ?_mvar.522600hε1:_fvar.521866 ≤ 1 / 2 := min_le_left ?_mvar.526121 ?_mvar.526122hε2:_fvar.521866 ≤ (2 - _fvar.301711 ^ 2) / 10 := min_le_right ?_mvar.526555 ?_mvar.526556⊢ x ^ 2 + 5 * ε < 2 All goals completed! 🐙 E:Set Chapter5.Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds _fvar.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h: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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.upperBound_def _fvar.284524 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.284524 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.bddAbove_def _fvar.284524)))) (Exists.intro 2 _fvar.284718)claim2:1 ∈ _fvar.284524 := 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.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := Chapter5.Real.exist_sqrt_two._proof_3 _fvar.295187 _fvar.301623claim4:_fvar.301711 ≥ 1 := Chapter5.Real.exist_sqrt_two._proof_4 _fvar.295335 _fvar.302023claim5:_fvar.301711 ≤ 2 := Chapter5.Real.exist_sqrt_two._proof_5 _fvar.284718 _fvar.302023claim6:Chapter5.Real.IsPos _fvar.301711 := Eq.mpr (id (congrArg (fun _a => _a) (propext (Chapter5.Real.isPos_iff _fvar.301711)))) (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.301711) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.301711 (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.301711 ^ 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.301711 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.301711) (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.301711 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.301711 (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.308148)) (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.284524 := ?_mvar.284717claim1':BddAbove _fvar.284524 := ?_mvar.295186claim2:1 ∈ _fvar.284524 := ?_mvar.295334claim2':E.Nonemptyx:Chapter5.Real := match Chapter5.ExtendedReal.sup _fvar.284524 with | Chapter5.ExtendedReal.neg_infty => 0 | Chapter5.ExtendedReal.real x => x | Chapter5.ExtendedReal.infty => 0claim3:IsLUB _fvar.284524 _fvar.301711 := ?_mvar.302022claim4:_fvar.301711 ≥ 1 := ?_mvar.308147claim5:_fvar.301711 ≤ 2 := ?_mvar.314301claim6:Chapter5.Real.IsPos _fvar.301711 := ?_mvar.319850h:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(_fvar.301711 + _fvar.535757) ^ 2 < 2 := Trans.trans (Trans.trans (Trans.trans ?_mvar.536461 ?_mvar.536809) ?_mvar.537327) _fvar.535779⊢ 0 ≤ x + ε; All goals completed! 🐙 have claim10 : x + ε ≤ x := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙

Remark 5.5.13

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

Helper lemma for Exercise 5.5.1.

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

Exercise 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! 🐙

Exercise 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! 🐙
/- Use the notion of supremum in this section to define a Mathlib `sSup` operation -/ noncomputable instance Real.inst_SupSet : SupSet Real where sSup E := ((ExtendedReal.sup E):Real)

Use the SupSet.sSup.{u_1} {α : Type u_1} [self : SupSet α] : Set α → αsSup operation to build a conditionally complete lattice structure on 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