Analysis
5.5. The least upper bound property

Imports

import Mathlib.Tactic
import Analysis.Section_5_4

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 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 := byx:Realy:Realz:Real⊢ z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y simp [Real.Icc_def]All goals completed! 🐙

/-- Example 5.5.2 -/
declaration uses `sorry`example (M: Real) : M ∈ upperBounds (.Icc 0 1) ↔ M ≥ 1 := byM:Real⊢ M ∈ upperBounds (Set.Icc 0 1) ↔ M ≥ 1 sorryAll 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 : Real, M ∈ upperBounds (.Ioi 0) := by⊢ ¬∃ M, M ∈ upperBounds (Set.Ioi 0) sorryAll goals completed! 🐙/-- Example 5.5.4 -/
declaration uses `sorry`example : ∀ M, M ∈ upperBounds (∅ : Set Real) := by⊢ ∀ (M : Real), M ∈ upperBounds ∅ sorryAll 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 := byM:RealM':Realh:M ≤ M'E:Set Realhb:M ∈ upperBounds E⊢ M' ∈ upperBounds E sorryAll goals completed! 🐙

Definition 5.5.5 (least upper bound). Here we use the 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 := byE:Set RealM:Real⊢ IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M rflAll goals completed! 🐙

              theorem Real.isGLB_def (E: Set Real) (M: Real) :
    IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M := byE:Set RealM:Real⊢ IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M rflAll goals completed! 🐙/-- Example 5.5.6 -/
declaration uses `sorry`example : IsLUB (.Icc 0 1) (1 : Real) := by⊢ IsLUB (Set.Icc 0 1) 1 sorryAll goals completed! 🐙/-- Example 5.5.7 -/
declaration uses `sorry`example : ¬∃ M, IsLUB (∅: Set Real) M := by⊢ ¬∃ M, IsLUB ∅ M sorryAll 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' := byE:Set RealM:RealM':Realh1:IsLUB E Mh2:IsLUB E M'⊢ M = M'
  grind [Real.isLUB_def]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 := byE: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 sorryAll 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' := byE: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' sorryAll 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 := bya:ℕ → ℚha:(↑a).IsCauchy⊢ (↑|a|).IsCauchy sorryAll 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| := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:LIM a = LIM b⊢ LIM |a| = LIM |b| sorryAll goals completed! 🐙theorem declaration uses `sorry`Real.LIM.abs_eq_pos {a: ℕ → ℚ} (h: LIM a > 0) (ha: (a:Sequence).IsCauchy):
    LIM a = LIM |a| := bya:ℕ → ℚh:LIM a > 0ha:(↑a).IsCauchy⊢ LIM a = LIM |a| sorryAll goals completed! 🐙theorem declaration uses `sorry`Real.LIM_abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy): |LIM a| = LIM |a| := bya:ℕ → ℚha:(↑a).IsCauchy⊢ |LIM a| = LIM |a| sorryAll 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 := byx:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∃ N, ∀ n ≥ N, ↑(a n) ≤ x⊢ LIM a ≤ x sorryAll 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) := byq:ℕ → ℚhq:∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)⊢ (↑q).IsCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1) sorryAll 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 := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
  set x₀ := Set.Nonempty.some hEn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.some⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
  observe hx₀ : x₀ ∈ En:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
  set ε := ((1/(n+1):ℚ):Real)n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
  have hpos : ε.IsPos := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E simp [isPos_iff, ε]n:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))⊢ 0 < ↑n + 1; positivityAll goals completed! 🐙
  apply existsUnique_of_exists_of_uniquehexn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehuniquen:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPos⊢ ∀ (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₂
  .hexn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E rw [bddAbove_def] at hboundhexn:ℕE:Set RealhE:E.Nonemptyhbound:∃ M, M ∈ upperBounds Ex₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E; obtain ⟨ M, hbound ⟩ := hboundhexn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds E⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
    choose K _ hK using le_mul hpos Mhexn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 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
    choose L' _ hL using le_mul hpos (-x₀)hexn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 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
    set L := -(L':ℤ)hexn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
    have claim1_1 : L * ε < x₀ := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E simp [L]n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'⊢ -(↑L' * ε) < x₀; linarithAll goals completed! 🐙
    have claim1_2 : L * ε ∉ upperBounds E := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E grind [upperBound_def]All goals completed! 🐙
    have claim1_3 : (K:Real) > (L:Real) := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
      contrapose! claim1_2n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑K ≤ ↑L⊢ ↑L * ε ∈ upperBounds E
      replace claim1_2 := mul_le_mul_left claim1_2 hposn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:ε * ↑K ≤ ε * ↑L⊢ ↑L * ε ∈ upperBounds E
      simp_rw [n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:ε * ↑K ≤ ε * ↑L⊢ ↑L * ε ∈ upperBounds Emul_comm] at claim1_2
      replace claim1_2 : M ≤ L * ε := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E orderAll goals completed! 🐙
      grind [upperBound_upper]All goals completed! 🐙
    have claim1_4 : ∃ m:ℤ, L < m ∧ m ≤ K ∧ m*ε ∈ upperBounds E ∧ (m-1)*ε ∉ upperBounds E := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E
      convert Real.upperBound_between (n := n) _ _ claim1_2convert_2n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ L < ↑Kconvert_3n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E
      .convert_2n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ L < ↑K qifyconvert_2n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑L < ↑K; rwa [←gt_iff_lt, gt_of_coe]convert_2n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝¹:K > 0hK:↑K * ε > ML':ℕh✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑↑K > ↑↑L
      simp [ε] at *convert_3n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑L'hpos:(↑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; apply upperBound_upper _ hboundn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))M:Realhbound:M ∈ upperBounds EK:ℕL':ℕL:ℤ := -↑L'hpos:(↑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)⁻¹; orderAll goals completed! 🐙
    choose m _ _ hm hm' using claim1_4hexn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤ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; use mhn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤ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*ε := byn:ℕE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E simp [ε]n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ↑m / (↑n + 1) = ↑m * (↑n + 1)⁻¹; field_simpAll goals completed! 🐙
    exact ⟨ byn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E convert hmAll goals completed! 🐙, byn:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E convert hm'h.e'_1.h.e'_5n:ℕE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:hE.some ∈ Eε:Real := ↑(1 / (↑n + 1))hpos:ε.IsPosM:Realhbound:M ∈ upperBounds EK:ℕh✝³:K > 0hK:↑K * ε > ML':ℕh✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤh✝¹:L < mh✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) = (↑m - 1) * ε; simp [this, sub_mul, ε]All goals completed! 🐙 ⟩
  grind [upperBound_discrete_unique]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) := byE: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)
    intro n hnE: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 ≥ N⊢ ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1) 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':ℕ⊢ n' ≥ N → |a n - a n'| ≤ 1 / (↑N + 1) hn'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)
    rw [abs_le]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)
    split_andsrefine_1E: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'refine_2E: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)
    .refine_1E: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' specialize hm1 nrefine_1E: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'; specialize hm2 n'refine_1E: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 := byE: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) rw [lt_of_coe]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); contrapose! hm2E: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; grind [upperBound_upper]All goals completed! 🐙
      have bound3 : 1/((n':ℚ)+1) ≤ 1/(N+1) := byE: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) gcongrAll goals completed! 🐙
      rw [←neg_le_neg_iff] at bound3refine_1E: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 - b) n' < a nbound3:-(1 / (↑N + 1)) ≤ -(1 / (↑n' + 1))⊢ -(1 / (↑N + 1)) ≤ a n - a n'; rw [Pi.sub_apply] at bound1refine_1E: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'; grindAll goals completed! 🐙
    specialize hm1 n'refine_2E: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); specialize hm2 nrefine_2E: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' := byE: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) rw [lt_of_coe]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'); contrapose! hm2E: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; grind [upperBound_upper]All goals completed! 🐙
    have bound2 : ((a-b) n) = a n - 1 / (n+1) := byE: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) simp [hb n]All goals completed! 🐙
    have bound3 : 1/((n+1):ℚ) ≤ 1/(N+1) := byE: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) gcongrAll goals completed! 🐙
    linarithAll 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 := byE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S
  -- This proof is written to follow the structure of the original text.
  set x₀ := hE.someE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.some⊢ ∃ S, IsLUB E S
  have hx₀ : x₀ ∈ E := hE.some_memE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ E⊢ ∃ S, IsLUB E S
  set m : ℕ → ℤ := fun n ↦ (LUB_claim1 n hE hbound).exists.chooseE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choose⊢ ∃ S, IsLUB E S
  set a : ℕ → ℚ := fun n ↦ (m n:ℚ) / (n+1)E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)⊢ ∃ S, IsLUB E S
  set b : ℕ → ℚ := fun n ↦ 1 / (n+1)E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)⊢ ∃ S, IsLUB E S
  have claim1 (n: ℕ) := LUB_claim1 n hE hboundE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E⊢ ∃ S, IsLUB E S
  have hb : (b:Sequence).IsCauchy := .harmonic'E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchy⊢ ∃ S, IsLUB E S
  have hm1 (n:ℕ) := (claim1 n).exists.choose_spec.1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds E⊢ ∃ S, IsLUB E S
  have hm2 (n:ℕ) : ¬((a - b) n: Real) ∈ upperBounds E := (claim1 n).exists.choose_spec.2E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∃ S, IsLUB E S
  have claim2 (N:ℕ) := LUB_claim2 N (byE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕ⊢ ∀ (n : ℕ), b n = 1 / (↑n + 1) aesopAll goals completed! 🐙) hm1 hm2
  have claim3 : (a:Sequence).IsCauchy := (LIM_of_Cauchy claim2).1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchy⊢ ∃ S, IsLUB E S
  set S := LIM aE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM a⊢ ∃ S, IsLUB E S; use ShE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM a⊢ IsLUB E S
  have claim4 : S = LIM (a - b) := byE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S
    have : LIM b = 0 := LIM.harmonicE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM athis:LIM b = 0⊢ S = LIM (a - b)
    simp [←LIM_sub claim3 hb, S, this]All goals completed! 🐙
  rw [isLUB_def, upperBound_def]hE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ (∀ x ∈ E, x ≤ S) ∧ ∀ M' ∈ upperBounds E, M' ≥ S
  split_andsh.refine_1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ x ∈ E, x ≤ Sh.refine_2E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ M' ∈ upperBounds E, M' ≥ S
  .h.refine_1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ x ∈ E, x ≤ S intro x hxh.refine_1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ E⊢ x ≤ S; apply LIM_of_ge claim3h.refine_1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ E⊢ ∀ (n : ℕ), ↑(a n) ≥ x; intro nh.refine_1E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ En:ℕ⊢ ↑(a n) ≥ x
    exact (upperBound_def E (a n)).mp (hm1 n) x hxAll goals completed! 🐙
  intro y hyh.refine_2E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds E⊢ y ≥ S
  have claim5 (n:ℕ) : y ≥ (a-b) n := byE:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S contrapose! hm2E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ∃ n, ↑((a - b) n) ∈ upperBounds E; use nhE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ↑((a - b) n) ∈ upperBounds E; apply upperBound_upper _ hyE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ y ≤ ↑((a - b) n); orderAll goals completed! 🐙
  rw [claim4]h.refine_2E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), y ≥ ↑((a - b) n)⊢ y ≥ LIM (a - b); apply LIM_of_le _ claim5E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Em:ℕ → ℤ := fun n ↦ ⋯.choosea:ℕ → ℚ := fun n ↦ ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n ↦ 1 / (↑n + 1)claim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehb:(↑b).IsCauchyhm1:∀ (n : ℕ), ↑(↑⋯.choose / (↑n + 1)) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |↑⋯.choose / (↑n + 1) - ↑⋯.choose / (↑n' + 1)| ≤ 1 / (↑N + 1)claim3:(↑a).IsCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), y ≥ ↑((a - b) n)⊢ (↑(a - b)).IsCauchy; solve_by_elim [Sequence.IsCauchy.sub]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 := neg_infty

              instance ExtendedReal.coe_real : Coe Real ExtendedReal where
  coe x := ExtendedReal.real xinstance ExtendedReal.real_coe : Coe ExtendedReal Real where
  coe X := match X with
  | neg_infty => 0
  | real x => x
  | infty => 0abbrev ExtendedReal.IsFinite (X : ExtendedReal) : Prop := match X with
  | neg_infty => False
  | real _ => True
  | infty => Falsetheorem ExtendedReal.finite_eq_coe {X: ExtendedReal} (hX: X.IsFinite) :
    X = ((X:Real):ExtendedReal) := byX:ExtendedRealhX:X.IsFinite⊢ X =
  real
    (match X with
    | neg_infty => 0
    | real x => x
    | infty => 0)
  cases Xneg_inftyhX:neg_infty.IsFinite⊢ neg_infty =
  real
    (match neg_infty with
    | neg_infty => 0
    | real x => x
    | infty => 0)realx✝:RealhX:(real x✝).IsFinite⊢ real x✝ =
  real
    (match real x✝ with
    | neg_infty => 0
    | real x => x
    | infty => 0)inftyhX:infty.IsFinite⊢ infty =
  real
    (match infty with
    | neg_infty => 0
    | real x => x
    | infty => 0) <;>neg_inftyhX:neg_infty.IsFinite⊢ neg_infty =
  real
    (match neg_infty with
    | neg_infty => 0
    | real x => x
    | infty => 0)realx✝:RealhX:(real x✝).IsFinite⊢ real x✝ =
  real
    (match real x✝ with
    | neg_infty => 0
    | real x => x
    | infty => 0)inftyhX:infty.IsFinite⊢ infty =
  real
    (match infty with
    | neg_infty => 0
    | real x => x
    | infty => 0) try simp [IsFinite] at hXAll goals completed! 🐙
  simpAll goals completed! 🐙

Definition 5.5.10 (Supremum)

open Classical in

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 ∅ = ⊥ := by⊢ sup ∅ = ⊥ simp [sup]All goals completed! 🐙

Definition 5.5.10 (Supremum)

theorem ExtendedReal.sup_of_unbounded {E: Set Real} (hb: ¬ BddAbove E) : sup E = ⊤ := byE:Set Realhb:¬BddAbove E⊢ sup E = ⊤
  have hE : E.Nonempty := byE:Set Realhb:¬BddAbove E⊢ sup E = ⊤ contrapose! hbE:Set Realhb:E = ∅⊢ BddAbove E; simp [hb]All goals completed! 🐙
  simp [sup, hE, hb]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) := byE:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E
  (match sup E with
  | neg_infty => 0
  | real x => x
  | infty => 0)
  simp [hnon, hb, sup]E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E ⋯.choose; exact (Real.LUB_exist hnon hb).choose_specAll goals completed! 🐙

theorem ExtendedReal.sup_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) :
    (sup E).IsFinite := byE:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ (sup E).IsFinite simp [sup, hnon, hb, IsFinite]All goals completed! 🐙

Proposition 5.5.12

theorem declaration uses `sorry`Real.exist_sqrt_two : ∃ x:Real, x^2 = 2 := by⊢ ∃ x, x ^ 2 = 2
  -- This proof is written to follow the structure of the original text.
  set E := { y:Real | y ≥ 0 ∧ y^2 < 2 }E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∃ x, x ^ 2 = 2
  have claim1: 2 ∈ upperBounds E := by⊢ ∃ x, x ^ 2 = 2
    rw [upperBound_def]E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∀ x ∈ E, x ≤ 2
    intro y hyE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:y ∈ E⊢ y ≤ 2; simp [E] at hyE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:0 ≤ y ∧ y ^ 2 < 2⊢ y ≤ 2; contrapose! hyE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < y⊢ 0 ≤ y → 2 ≤ y ^ 2
    intro hposE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ y ^ 2
    calc
      _ ≤ 2 * 2 := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ 2 * 2 norm_numAll goals completed! 🐙
      _ ≤ y * y := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 * 2 ≤ y * y gcongrAll goals completed! 🐙
      _ = y^2 := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ y * y = y ^ 2 ringAll goals completed! 🐙
  have claim1' : BddAbove E := by⊢ ∃ x, x ^ 2 = 2 rw [bddAbove_def]E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds E⊢ ∃ M, M ∈ upperBounds E; use 2All goals completed! 🐙
  have claim2: 1 ∈ E := by⊢ ∃ x, x ^ 2 = 2 simp [E]All goals completed! 🐙
  observe claim2': E.NonemptyE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonempty⊢ ∃ x, x ^ 2 = 2
  set x := ((ExtendedReal.sup E):Real)E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0⊢ ∃ x, x ^ 2 = 2
  have claim3 : IsLUB E x := by⊢ ∃ x, x ^ 2 = 2 grind [ExtendedReal.sup_of_bounded]All goals completed! 🐙
  have claim4 : x ≥ 1 := by⊢ ∃ x, x ^ 2 = 2 grind [isLUB_def, upperBound_def]All goals completed! 🐙
  have claim5 : x ≤ 2 := by⊢ ∃ x, x ^ 2 = 2 grind [isLUB_def]All goals completed! 🐙
  have claim6 : x.IsPos := by⊢ ∃ x, x ^ 2 = 2 rw [isPos_iff]E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2⊢ x > 0; linarithAll goals completed! 🐙
  use xhE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPos⊢ x ^ 2 = 2; obtain h | h | h := trichotomous' (x^2) 2h.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2⊢ x ^ 2 = 2h.inr.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2⊢ x ^ 2 = 2h.inr.inrE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 = 2⊢ x ^ 2 = 2
  .h.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2⊢ x ^ 2 = 2 have claim11: ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 - 4*ε > 2 := by⊢ ∃ x, x ^ 2 = 2
      set ε := min (1/2) ((x^2-2)/8)E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2
      have hx : x^2 - 2 > 0 := by⊢ ∃ x, x ^ 2 = 2 linarithAll goals completed! 🐙
      have hε : 0 < ε := by⊢ ∃ x, x ^ 2 = 2 positivityAll goals completed! 🐙
      observe hε1: ε ≤ 1/2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2
      observe hε2: ε ≤ (x^2-2)/8E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε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
      refine' ⟨ ε, hε, _, _ ⟩refine'_1E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ ε < 1refine'_2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε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 <;>refine'_1E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ 1 / 2hε2:min (1 / 2) ((x ^ 2 - 2) / 8) ≤ (x ^ 2 - 2) / 8⊢ ε < 1refine'_2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε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 linarithAll goals completed! 🐙
    choose ε hε1 hε2 hε3 using claim11h.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh: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 + ε * ε := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ (x - ε) ^ 2 = x ^ 2 - 2 * ε * x + ε * ε ringAll goals completed! 🐙
      _ ≥ x^2 - 2 * ε * 2 + 0 * 0 := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * x + ε * ε ≥ x ^ 2 - 2 * ε * 2 + 0 * 0 gcongrAll goals completed! 🐙
      _ = x^2 - 4 * ε := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * 2 + 0 * 0 = x ^ 2 - 4 * ε ringAll goals completed! 🐙
      _ > 2 := hε3
    have why (y:Real) (hy: y ∈ E) : x - ε ≥ y := by⊢ ∃ x, x ^ 2 = 2 sorryAll goals completed! 🐙
    have claim13: x-ε ∈ upperBounds E := by⊢ ∃ x, x ^ 2 = 2 rwa [upperBound_def]E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2claim12:(x - ε) ^ 2 > 2why:∀ y ∈ E, x - ε ≥ y⊢ ∀ x_1 ∈ E, x_1 ≤ x - ε
    have claim14: x ≤ x-ε := by⊢ ∃ x, x ^ 2 = 2 grind [isLUB_def]All goals completed! 🐙
    linarithAll goals completed! 🐙
  .h.inr.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2⊢ x ^ 2 = 2 have claim7 : ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 + 5*ε < 2 := by⊢ ∃ x, x ^ 2 = 2
      set ε := min (1/2) ((2-x^2)/10)E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2
      have hx : 2 - x^2 > 0 := by⊢ ∃ x, x ^ 2 = 2 linarithAll goals completed! 🐙
      have hε: 0 < ε := by⊢ ∃ x, x ^ 2 = 2 positivityAll goals completed! 🐙
      have hε1: ε ≤ 1/2 := min_le_left _ _E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2
      have hε2: ε ≤ (2 - x^2)/10 := min_le_right _ _E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2
      refine ⟨ ε, hε, ?_, ?_ ⟩refine_1E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ ε < 1refine_2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ x ^ 2 + 5 * ε < 2 <;>refine_1E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ ε < 1refine_2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ x ^ 2 + 5 * ε < 2 linarithAll goals completed! 🐙
    choose ε hε1 hε2 hε3 using claim7h.inr.inlE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh: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)*ε + ε*ε := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ (x + ε) ^ 2 = x ^ 2 + 2 * x * ε + ε * ε ringAll goals completed! 🐙
      _ ≤ x^2 + (2*2)*ε + 1*ε := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * x * ε + ε * ε ≤ x ^ 2 + 2 * 2 * ε + 1 * ε gcongrAll goals completed! 🐙
      _ = x^2 + 5*ε := byE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * 2 * ε + 1 * ε = x ^ 2 + 5 * ε ringAll goals completed! 🐙
      _ < 2 := hε3
    have claim9 : x + ε ∈ E := by⊢ ∃ x, x ^ 2 = 2 simp [E, claim8]E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := 
  match ExtendedReal.sup E with
  | ExtendedReal.neg_infty => 0
  | ExtendedReal.real x => x
  | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.IsPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(x + ε) ^ 2 < 2⊢ 0 ≤ x + ε; linarithAll goals completed! 🐙
    have claim10 : x + ε ≤ x := by⊢ ∃ x, x ^ 2 = 2 grind [isLUB_def, upperBound_def]All goals completed! 🐙
    linarithAll goals completed! 🐙
  assumptionAll goals completed! 🐙

Remark 5.5.13

theorem declaration uses `sorry`Real.exist_irrational : ∃ x:Real, ¬ ∃ q:ℚ, x = (q:Real) := by⊢ ∃ x, ¬∃ q, x = ↑q sorryAll 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) := byE:Set RealM:Realh:IsLUB E M⊢ IsGLB (-E) (-M) sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Real.GLB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddBelow E): ∃ S, IsGLB E S := byE:Set RealhE:E.Nonemptyhbound:BddBelow E⊢ ∃ S, IsGLB E S
  sorryAll 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 ∅ = ⊤ := by⊢ inf ∅ = ⊤ simp [inf]All goals completed! 🐙theorem ExtendedReal.inf_of_unbounded {E: Set Real} (hb: ¬ BddBelow E) : inf E = ⊥ := byE:Set Realhb:¬BddBelow E⊢ inf E = ⊥
  have hE : E.Nonempty := byE:Set Realhb:¬BddBelow E⊢ inf E = ⊥ contrapose! hbE:Set Realhb:E = ∅⊢ BddBelow E; simp [hb]All goals completed! 🐙
  simp [inf, hE, hb]All goals completed! 🐙theorem ExtendedReal.inf_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) :
    IsGLB E (inf E) := byE:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E
  (match inf E with
  | neg_infty => 0
  | real x => x
  | infty => 0) simp [hnon, hb, inf]E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E ⋯.choose; exact (Real.GLB_exist hnon hb).choose_specAll goals completed! 🐙theorem ExtendedReal.inf_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) :
    (inf E).IsFinite := byE:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ (inf E).IsFinite simp [inf, hnon, hb, 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) := byx:Realy:Realhxy:x < y⊢ ∃ z, x < z ∧ z < y ∧ ¬∃ q, z = ↑q sorryAll 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 sSup operation to build a conditionally complete lattice structure on Real.

noncomputable instance Real.inst_conditionallyCompleteLattice :
    ConditionallyCompleteLattice Real :=
  conditionallyCompleteLatticeOfLatticeOfsSup Real
  (by⊢ ∀ (s : Set Real), BddAbove s → s.Nonempty → IsLUB s (sSup s) intross✝:Set Reala✝¹:BddAbove s✝a✝:s✝.Nonempty⊢ IsLUB s✝ (sSup s✝); solve_by_elim [ExtendedReal.sup_of_bounded]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 hb

end Chapter5