Analysis I, Section 6.4: Limsup, liminf, and limit points

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:

Lim sup and lim inf of sequences
Limit points of sequences
Comparison and squeeze tests
Completeness of the reals

abbrev Real.Adherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) := ∃ n ≥ a.m, ε.Close (a n) x

abbrev Real.ContinuallyAdherent (ε:ℝ) (a:Chapter6.Sequence) (x:ℝ) :=
  ∀ N ≥ a.m, ε.Adherent (a.from N) x

namespace Chapter6open EReal

abbrev Sequence.LimitPoint (a:Sequence) (x:ℝ) : Prop :=
  ∀ ε > (0:ℝ), ε.ContinuallyAdherent a x

theorem declaration uses `sorry`Sequence.limit_point_def (a:Sequence) (x:ℝ) :
  a.LimitPoint x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a n - x| ≤ ε := bya:Sequencex:ℝ⊢ a.LimitPoint x ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    unfold LimitPoint Real.ContinuallyAdherent Real.Adherenta:Sequencex:ℝ⊢ (∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ (a.from N).m, ε.Close ((a.from N).seq n) x) ↔ ∀ ε > 0, ∀ N ≥ a.m, ∃ n ≥ N, |a.seq n - x| ≤ ε
    sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_3 : Sequence := (fun (n:ℕ) ↦ 1 - (10:ℝ)^(-(n:ℤ)-1))

Example 6.4.3

declaration uses `sorry`example : (0.1:ℝ).Adherent Example_6_4_3 0.8 := by⊢ Real.Adherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses `sorry`example : ¬ (0.1:ℝ).ContinuallyAdherent Example_6_4_3 0.8 := by⊢ ¬Real.ContinuallyAdherent 0.1 Example_6_4_3 0.8 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses `sorry`example : (0.1:ℝ).ContinuallyAdherent Example_6_4_3 1 := by⊢ Real.ContinuallyAdherent 0.1 Example_6_4_3 1 sorryAll goals completed! 🐙

Example 6.4.3

declaration uses `sorry`example : Example_6_4_3.LimitPoint 1 := by⊢ Example_6_4_3.LimitPoint 1 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_4 : Sequence :=
  (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

Example 6.4.4

declaration uses `sorry`example : (0.1:ℝ).Adherent Example_6_4_4 1 := by⊢ Real.Adherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses `sorry`example : (0.1:ℝ).ContinuallyAdherent Example_6_4_4 1 := by⊢ Real.ContinuallyAdherent 0.1 Example_6_4_4 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses `sorry`example : Example_6_4_4.LimitPoint 1 := by⊢ Example_6_4_4.LimitPoint 1 sorryAll goals completed! 🐙

Example 6.4.4

declaration uses `sorry`example : Example_6_4_4.LimitPoint (-1) := by⊢ Example_6_4_4.LimitPoint (-1) sorryAll goals completed! 🐙

Example 6.4.4

declaration uses `sorry`example : ¬ Example_6_4_4.LimitPoint 0 := by⊢ ¬Example_6_4_4.LimitPoint 0 sorryAll goals completed! 🐙

Proposition 6.4.5 / Exercise 6.4.1

theorem declaration uses `sorry`Sequence.limit_point_of_limit {a:Sequence} {x:ℝ} (h: a.TendsTo x) : a.LimitPoint x := bya:Sequencex:ℝh:a.TendsTo x⊢ a.LimitPoint x
  sorryAll goals completed! 🐙

A technical issue uncovered by the formalization: the upper and lower sequences of a real sequence take values in the extended reals rather than the reals, so the definitions need to be adjusted accordingly.

noncomputable abbrev Sequence.upperseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).sup

noncomputable abbrev Sequence.limsup (a:Sequence) : EReal :=
  sInf { x | ∃ N ≥ a.m, x = a.upperseq N }

noncomputable abbrev Sequence.lowerseq (a:Sequence) : ℤ → EReal := fun N ↦ (a.from N).inf

noncomputable abbrev Sequence.liminf (a:Sequence) : EReal :=
  sSup { x | ∃ N ≥ a.m, x = a.lowerseq N }

noncomputable abbrev Example_6_4_7 : Sequence := (fun (n:ℕ) ↦ (-1:ℝ)^n * (1 + (10:ℝ)^(-(n:ℤ)-1)))

declaration uses `sorry`example (n:ℕ) :
    Example_6_4_7.upperseq n = if Even n then 1 + (10:ℝ)^(-(n:ℤ)-1) else 1 + (10:ℝ)^(-(n:ℤ)-2) := byn:ℕ⊢ Example_6_4_7.upperseq ↑n = ↑(if Even n then 1 + 10 ^ (-↑n - 1) else 1 + 10 ^ (-↑n - 2))
  sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_7.limsup = 1 := by⊢ Example_6_4_7.limsup = 1 sorryAll goals completed! 🐙

declaration uses `sorry`example (n:ℕ) :
    Example_6_4_7.lowerseq n
    = if Even n then -(1 + (10:ℝ)^(-(n:ℤ)-2)) else -(1 + (10:ℝ)^(-(n:ℤ)-1)) := byn:ℕ⊢ Example_6_4_7.lowerseq ↑n = ↑(if Even n then -(1 + 10 ^ (-↑n - 2)) else -(1 + 10 ^ (-↑n - 1)))
  sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_7.liminf = -1 := by⊢ Example_6_4_7.liminf = -1 sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_7.sup = (1.1:ℝ) := by⊢ Example_6_4_7.sup = ↑1.1 sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_7.inf = (-1.01:ℝ) := by⊢ Example_6_4_7.inf = ↑(-1.01) sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_8 : Sequence := (fun (n:ℕ) ↦ if Even n then (n+1:ℝ) else -(n:ℝ)-1)

declaration uses `sorry`example (n:ℕ) : Example_6_4_8.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_8.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_8.limsup = ⊤ := by⊢ Example_6_4_8.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses `sorry`example (n:ℕ) : Example_6_4_8.lowerseq n = ⊥ := byn:ℕ⊢ Example_6_4_8.lowerseq ↑n = ⊥ sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_8.liminf = ⊥ := by⊢ Example_6_4_8.liminf = ⊥ sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_9 : Sequence :=
  (fun (n:ℕ) ↦ if Even n then (n+1:ℝ)⁻¹ else -(n+1:ℝ)⁻¹)

declaration uses `sorry`example (n:ℕ) : Example_6_4_9.upperseq n = if Even n then (n+1:ℝ)⁻¹ else -(n+2:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.upperseq ↑n = ↑(if Even n then (↑n + 1)⁻¹ else -(↑n + 2)⁻¹) sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_9.limsup = 0 := by⊢ Example_6_4_9.limsup = 0 sorryAll goals completed! 🐙

declaration uses `sorry`example (n:ℕ) : Example_6_4_9.lowerseq n = if Even n then -(n+2:ℝ)⁻¹ else -(n+1:ℝ)⁻¹ := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑(if Even n then -(↑n + 2)⁻¹ else -(↑n + 1)⁻¹) sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_9.liminf = 0 := by⊢ Example_6_4_9.liminf = 0 sorryAll goals completed! 🐙

noncomputable abbrev Example_6_4_10 : Sequence := (fun (n:ℕ) ↦ (n+1:ℝ))

declaration uses `sorry`example (n:ℕ) : Example_6_4_10.upperseq n = ⊤ := byn:ℕ⊢ Example_6_4_10.upperseq ↑n = ⊤ sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_9.limsup = ⊤ := by⊢ Example_6_4_9.limsup = ⊤ sorryAll goals completed! 🐙

declaration uses `sorry`example (n:ℕ) : Example_6_4_9.lowerseq n = n+1 := byn:ℕ⊢ Example_6_4_9.lowerseq ↑n = ↑n + 1 sorryAll goals completed! 🐙

declaration uses `sorry`example : Example_6_4_9.liminf = ⊤ := by⊢ Example_6_4_9.liminf = ⊤ sorryAll goals completed! 🐙

Proposition 6.4.12(a)

theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  -- This proof is written to follow the structure of the original text.
  simp only [limsup, sInf_lt_iff] at ha:Sequencex:ERealh:∃ a_1 ∈ {x | ∃ N ≥ a.m, x = a.upperseq N}, a_1 < x⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  obtain ⟨y, hy, ha⟩ := ha:Sequencex:ERealy:ERealhy:y ∈ {x | ∃ N ≥ a.m, x = a.upperseq N}ha:y < x⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  obtain ⟨N, hN, hNy⟩ := hya:Sequencex:ERealy:ERealha:y < xN:ℤhN:N ≥ a.mhNy:y = a.upperseq N⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x
  rw [hNy] at haa:Sequencex:ERealy:ERealN:ℤha:a.upperseq N < xhN:N ≥ a.mhNy:y = a.upperseq N⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x; use Nha:Sequencex:ERealy:ERealN:ℤha:a.upperseq N < xhN:N ≥ a.mhNy:y = a.upperseq N⊢ N ≥ a.m ∧ ∀ n ≥ N, ↑(a.seq n) < x
  simp [hN, upperseq] at ha ⊢ha:Sequencex:ERealy:ERealN:ℤha:(a.from N).sup < xhN:N ≥ a.mhNy:y = a.upperseq N⊢ ∀ (n : ℤ), N ≤ n → ↑(a.seq n) < x; intro n _ha:Sequencex:ERealy:ERealN:ℤha:(a.from N).sup < xhN:N ≥ a.mhNy:y = a.upperseq Nn:ℤa✝:N ≤ n⊢ ↑(a.seq n) < x
  have hn' : n ≥ (a.from N).m := bya:Sequencex:ERealh:x > a.limsup⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) < x grindAll goals completed! 🐙
  convert lt_of_le_of_lt ((a.from N).le_sup hn') ha using 1h.e'_3a:Sequencex:ERealy:ERealN:ℤha:(a.from N).sup < xhN:N ≥ a.mhNy:y = a.upperseq Nn:ℤa✝:N ≤ nhn':n ≥ (a.from N).m := gt_limsup_bounds._proof_1 N hN n a✝⊢ ↑(a.seq n) = ↑((a.from N).seq n)
  grindAll goals completed! 🐙

Proposition 6.4.12(a)

theorem declaration uses `sorry`Sequence.lt_liminf_bounds {a:Sequence} {y:EReal} (h: y < a.liminf) :
    ∃ N ≥ a.m, ∀ n ≥ N, a n > y := bya:Sequencey:ERealh:y < a.liminf⊢ ∃ N ≥ a.m, ∀ n ≥ N, ↑(a.seq n) > y
  sorryAll goals completed! 🐙

Proposition 6.4.12(b)

theorem Sequence.lt_limsup_bounds {a:Sequence} {x:EReal} (h: x < a.limsup) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n > x := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x
  -- This proof is written to follow the structure of the original text.
  have hx : x < a.upperseq N := bya:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) > x apply lt_of_lt_of_le h (sInf_le _)a:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ a.upperseq N ∈ {x | ∃ N ≥ a.m, x = a.upperseq N}; simpa:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.m⊢ ∃ N_1, a.m ≤ N_1 ∧ a.upperseq N = a.upperseq N_1; use NAll goals completed! 🐙
  choose n hn hxn _ using exists_between_lt_sup hxa:Sequencex:ERealh:x < a.limsupN:ℤhN:N ≥ a.mhx:x < a.upperseq N := 
  lt_of_lt_of_le h
    (sInf_le
      (Eq.mpr
        (id
          (congrFun'
            (congrArg Membership.mem
              (congrArg setOf
                (funext fun x =>
                  congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = a.upperseq N)))))
            (a.upperseq N)))
        (Exists.intro N ⟨hN, Eq.refl (a.upperseq N)⟩)))n:ℤhn:n ≥ (a.from N).mhxn:x < ↑((a.from N).seq n)a✝:↑((a.from N).seq n) ≤ (a.from N).sup⊢ ∃ n ≥ N, ↑(a.seq n) > x
  grindAll goals completed! 🐙

Proposition 6.4.12(b)

theorem declaration uses `sorry`Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:ℤ} (hN: N ≥ a.m) :
    ∃ n ≥ N, a n < x := bya:Sequencex:ERealh:x > a.liminfN:ℤhN:N ≥ a.m⊢ ∃ n ≥ N, ↑(a.seq n) < x
  sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := bya:Sequence⊢ a.inf ≤ a.liminf sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := bya:Sequence⊢ a.liminf ≤ a.limsup sorryAll goals completed! 🐙

Proposition 6.4.12(c) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.limsup_le_sup (a:Sequence) : a.limsup ≤ a.sup := bya:Sequence⊢ a.limsup ≤ a.sup sorryAll goals completed! 🐙

Proposition 6.4.12(d) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.limit_point_between_liminf_limsup {a:Sequence} {c:ℝ} (h: a.LimitPoint c) :
  a.liminf ≤ c ∧ c ≤ a.limsup := bya:Sequencec:ℝh:a.LimitPoint c⊢ a.liminf ≤ ↑c ∧ ↑c ≤ a.limsup
  sorryAll goals completed! 🐙

Proposition 6.4.12(e) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.limit_point_of_limsup {a:Sequence} {L_plus:ℝ} (h: a.limsup = L_plus) :
    a.LimitPoint L_plus := bya:SequenceL_plus:ℝh:a.limsup = ↑L_plus⊢ a.LimitPoint L_plus
  sorryAll goals completed! 🐙

Proposition 6.4.12(e) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.limit_point_of_liminf {a:Sequence} {L_minus:ℝ} (h: a.liminf = L_minus) :
    a.LimitPoint L_minus := bya:SequenceL_minus:ℝh:a.liminf = ↑L_minus⊢ a.LimitPoint L_minus
  sorryAll goals completed! 🐙

Proposition 6.4.12(f) / Exercise 6.4.3

theorem declaration uses `sorry`Sequence.tendsTo_iff_eq_limsup_liminf {a:Sequence} (c:ℝ) :
  a.TendsTo c ↔ a.liminf = c ∧ a.limsup = c := bya:Sequencec:ℝ⊢ a.TendsTo c ↔ a.liminf = ↑c ∧ a.limsup = ↑c
  sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses `sorry`Sequence.sup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.sup ≤ b.sup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.sup ≤ b.sup sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses `sorry`Sequence.inf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.inf ≤ b.inf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.inf ≤ b.inf sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses `sorry`Sequence.limsup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.limsup ≤ b.limsup := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.limsup ≤ b.limsup sorryAll goals completed! 🐙

Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4

theorem declaration uses `sorry`Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
    a.liminf ≤ b.liminf := bya:Sequenceb:Sequencehm:a.m = b.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n⊢ a.liminf ≤ b.liminf sorryAll goals completed! 🐙

Corollary 6.4.14 (Squeeze test) / Exercise 6.4.5

theorem declaration uses `sorry`Sequence.lim_of_between {a b c:Sequence} {L:ℝ} (hm: b.m = a.m ∧ c.m = a.m)
  (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: c.TendsTo L) :
    b.TendsTo L := bya:Sequenceb:Sequencec:SequenceL:ℝhm:b.m = a.m ∧ c.m = a.mhab:∀ n ≥ a.m, a.seq n ≤ b.seq n ∧ b.seq n ≤ c.seq nha:a.TendsTo Lhb:c.TendsTo L⊢ b.TendsTo L sorryAll goals completed! 🐙

Example 6.4.15

declaration uses `sorry`example : ((fun (n:ℕ) ↦ 2/(n+1:ℝ)):Sequence).TendsTo 0 := by⊢ (↑fun n => 2 / (↑n + 1)).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses `sorry`example : ((fun (n:ℕ) ↦ -2/(n+1:ℝ)):Sequence).TendsTo 0 := by⊢ (↑fun n => -2 / (↑n + 1)).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (-1)^n/(n+1:ℝ) + 1 / (n+1)^2):Sequence).TendsTo 0 := by⊢ (↑fun n => (-1) ^ n / (↑n + 1) + 1 / (↑n + 1) ^ 2).TendsTo 0
  sorryAll goals completed! 🐙

Example 6.4.15

declaration uses `sorry`example : ((fun (n:ℕ) ↦ (2:ℝ)^(-(n:ℤ))):Sequence).TendsTo 0 := by⊢ (↑fun n => 2 ^ (-↑n)).TendsTo 0
  sorryAll goals completed! 🐙

abbrev Sequence.abs (a:Sequence) : Sequence where
  m := a.m
  seq n := |a n|
  vanish n hn := bya:Sequencen:ℤhn:n < a.m⊢ |a.seq n| = 0 simp [a.vanish n hn]All goals completed! 🐙

Corollary 6.4.17 (Zero test for sequences) / Exercise 6.4.7

theorem declaration uses `sorry`Sequence.tendsTo_zero_iff (a:Sequence) :
  a.TendsTo (0:ℝ) ↔ a.abs.TendsTo (0:ℝ) := bya:Sequence⊢ a.TendsTo 0 ↔ a.abs.TendsTo 0
  sorryAll goals completed! 🐙

This helper lemma, implicit in the textbook proofs of Theorem 6.4.18 and Theorem 6.6.8, is made explicit here.

theorem Sequence.finite_limsup_liminf_of_bounded {a:Sequence} (hbound: a.IsBounded) :
    (∃ L_plus:ℝ, a.limsup = L_plus) ∧ (∃ L_minus:ℝ, a.liminf = L_minus) := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  choose M hMpos hbound using hbounda:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy M⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
  have hlimsup_bound : a.limsup ≤ M := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply a.limsup_le_sup.trans (sup_le_upper _)a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy M⊢ ∀ n ≥ a.m, ↑(a.seq n) ≤ ↑M
    intro n hNa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mn:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≤ ↑M; simpa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mn:ℤhN:n ≥ a.m⊢ a.seq n ≤ M
    exact (le_abs_self _).trans (hbound n)All goals completed! 🐙
  have hliminf_bound : -M ≤ a.liminf := bya:Sequencehbound:a.IsBounded⊢ (∃ L_plus, a.limsup = ↑L_plus) ∧ ∃ L_minus, a.liminf = ↑L_minus
    apply (inf_ge_lower _).trans a.inf_le_liminfa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))⊢ ∀ n ≥ a.m, ↑(a.seq n) ≥ -↑M
    intro n hNa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))n:ℤhN:n ≥ a.m⊢ ↑(a.seq n) ≥ -↑M; simp [←coe_neg]a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))n:ℤhN:n ≥ a.m⊢ -M ≤ a.seq n; rw [neg_le]a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))n:ℤhN:n ≥ a.m⊢ -a.seq n ≤ M
    exact (neg_le_abs _).trans (hbound n)All goals completed! 🐙
  split_andsrefine_1a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ ∃ L_plus, a.limsup = ↑L_plusrefine_2a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ ∃ L_minus, a.liminf = ↑L_minus
  .refine_1a:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ ∃ L_plus, a.limsup = ↑L_plus use a.limsup.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.limsup = ↑a.limsup.toReal
    symmha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ ↑a.limsup.toReal = a.limsup; apply coe_toRealh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.limsup ≠ ⊤h.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.limsup ≠ ⊥
    .h.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.limsup ≠ ⊤ contrapose! hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)hlimsup_bound:a.limsup = ⊤⊢ ↑M < a.limsup; simp [hlimsup_bound]All goals completed! 🐙
    replace hliminf_bound := hliminf_bound.trans a.liminf_le_limsuph.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.limsup := LE.le.trans _fvar.107677 (liminf_le_limsup a)⊢ a.limsup ≠ ⊥
    contrapose! hliminf_boundh.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:a.limsup = ⊥⊢ a.limsup < -↑M; simp [hliminf_bound, ←coe_neg]All goals completed! 🐙
  use a.liminf.toRealha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.liminf = ↑a.liminf.toReal; symmha:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ ↑a.liminf.toReal = a.liminf; apply coe_toRealh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.liminf ≠ ⊤h.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.liminf ≠ ⊥
  .h.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)⊢ a.liminf ≠ ⊤ apply a.liminf_le_limsup.trans at hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)hlimsup_bound:a.liminf ≤ ↑M⊢ a.liminf ≠ ⊤
    contrapose! hlimsup_boundh.hxa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhliminf_bound:-↑M ≤ a.liminf := 
  LE.le.trans
    (inf_ge_lower fun n hN =>
      Eq.mpr (id (Eq.trans ge_iff_le._simp_1 coe_le_coe_iff._simp_1))
        (Eq.mpr (id (congrArg (fun _a => _a) (propext neg_le))) (LE.le.trans (neg_le_abs (a.seq n)) (hbound n))))
    (inf_le_liminf a)hlimsup_bound:a.liminf = ⊤⊢ ↑M < a.liminf; simp [hlimsup_bound]All goals completed! 🐙
  contrapose! hliminf_boundh.h'xa:SequenceM:ℝhMpos:M ≥ 0hbound:a.BoundedBy Mhlimsup_bound:a.limsup ≤ ↑M := 
  LE.le.trans (limsup_le_sup a)
    (sup_le_upper fun n hN => Eq.mpr (id coe_le_coe_iff._simp_1) (LE.le.trans (le_abs_self (a.seq n)) (hbound n)))hliminf_bound:a.liminf = ⊥⊢ a.liminf < -↑M; simp [hliminf_bound, ←coe_neg]All goals completed! 🐙

Theorem 6.4.18 (Completeness of the reals)

theorem Sequence.Cauchy_iff_convergent (a:Sequence) :
  a.IsCauchy ↔ a.Convergent := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
  -- This proof is written to follow the structure of the original text.
  refine ⟨ ?_, IsCauchy.convergent ⟩a:Sequence⊢ a.IsCauchy → a.Convergent; intro ha:Sequenceh:a.IsCauchy⊢ a.Convergent
  have ⟨ ⟨ L_plus, hL_plus ⟩, ⟨ L_minus, hL_minus ⟩ ⟩ :=
    finite_limsup_liminf_of_bounded (bounded_of_cauchy h)a:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.Convergent
  use L_minusha:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ a.TendsTo L_minus; simp [tendsTo_iff_eq_limsup_liminf, hL_minus, hL_plus]ha:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minus⊢ L_plus = L_minus
  have hlow : 0 ≤ L_plus - L_minus := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
    have := a.liminf_le_limsupa:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:a.liminf ≤ a.limsup := liminf_le_limsup a⊢ 0 ≤ L_plus - L_minus; simp [hL_minus, hL_plus] at thisa:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minusthis:L_minus ≤ L_plus⊢ 0 ≤ L_plus - L_minus; grindAll goals completed! 🐙
  have hup (ε:ℝ) (hε: ε>0) : L_plus - L_minus ≤ 2*ε := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
    specialize h ε hεa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0h:ε.EventuallySteady a⊢ L_plus - L_minus ≤ 2 * ε; choose N hN hsteady using ha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)⊢ L_plus - L_minus ≤ 2 * ε
    have hN0 : N ≥ (a.from N).m := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent grindAll goals completed! 🐙
    have hN1 : (a.from N).seq N = a.seq N := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent grindAll goals completed! 🐙
    have h1 : (a N - ε:ℝ) ≤ (a.from N).inf := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      apply inf_ge_lowerha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≥ ↑(a.seq N - ε); grind [Real.dist_eq, abs_le',EReal.coe_le_coe_iff]All goals completed! 🐙
    have h2 : (a.from N).inf ≤ L_minus := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      simp_rw [a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)⊢ (a.from N).inf ≤ ↑L_minus←hL_minus, liminf, lowerseq]; apply le_sSupaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)⊢ (a.from N).inf ∈ {x | ∃ N ≥ a.m, x = (a.from N).inf}; simpaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).inf = (a.from N_1).inf; use NAll goals completed! 🐙
    have h3 : (a.from N).sup ≤ (a N + ε:ℝ) := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      apply sup_le_upperha:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))⊢ ∀ n ≥ (a.from N).m, ↑((a.from N).seq n) ≤ ↑(a.seq N + ε); grind [EReal.coe_le_coe_iff, Real.dist_eq, abs_le']All goals completed! 🐙
    have h4 : L_plus ≤ (a.from N).sup := bya:Sequence⊢ a.IsCauchy ↔ a.Convergent
      simp_rw [a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))h3:(a.from N).sup ≤ ↑(a.seq N + ε) := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N hsteady hN0 hN1)⊢ ↑L_plus ≤ (a.from N).sup←hL_plus, limsup, upperseq]; apply sInf_leaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))h3:(a.from N).sup ≤ ↑(a.seq N + ε) := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N hsteady hN0 hN1)⊢ (a.from N).sup ∈ {x | ∃ N ≥ a.m, x = (a.from N).sup}; simpaa:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h1:↑(a.seq N - ε) ≤ (a.from N).inf := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N hsteady hN0 hN1)h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))h3:(a.from N).sup ≤ ↑(a.seq N + ε) := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N hsteady hN0 hN1)⊢ ∃ N_1, a.m ≤ N_1 ∧ (a.from N).sup = (a.from N_1).sup; use NAll goals completed! 🐙
    replace h1 := h1.trans h2a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))h3:(a.from N).sup ≤ ↑(a.seq N + ε) := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N hsteady hN0 hN1)h4:↑L_plus ≤ (a.from N).sup := 
  Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
    (id
      (id
        (sInf_le
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                (a.from N).sup))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).sup⟩)))))h1:↑(a.seq N - ε) ≤ ↑L_minus := LE.le.trans _fvar.291008 h2⊢ L_plus - L_minus ≤ 2 * ε
    replace h4 := h4.trans h3a:SequenceL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)ε:ℝhε:ε > 0N:ℤhN:N ≥ a.mhsteady:ε.Steady (a.from N)hN0:N ≥ (a.from N).m := Cauchy_iff_convergent._proof_2 a N hNhN1:(a.from N).seq N = a.seq N := Cauchy_iff_convergent._proof_3 a N hN0h2:(a.from N).inf ≤ ↑L_minus := 
  Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
    (id
      (id
        (le_sSup
          (Eq.mpr
            (id
              (congrFun'
                (congrArg Membership.mem
                  (congrArg setOf
                    (funext fun x =>
                      congrArg Exists (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                (a.from N).inf))
            (Exists.intro N ⟨hN, Eq.refl (a.from N).inf⟩)))))h3:(a.from N).sup ≤ ↑(a.seq N + ε) := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N hsteady hN0 hN1)h1:↑(a.seq N - ε) ≤ ↑L_minus := LE.le.trans _fvar.291008 h2h4:↑L_plus ≤ ↑(a.seq N + ε) := LE.le.trans _fvar.367957 h3⊢ L_plus - L_minus ≤ 2 * ε
    grind [EReal.coe_le_coe_iff]All goals completed! 🐙
  obtain hlow | hlow := le_iff_lt_or_eq.mp hlowh.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hup:∀ ε > 0, L_plus - L_minus ≤ 2 * ε := 
  fun ε hε =>
    (fun N x =>
        have hN0 := Cauchy_iff_convergent._proof_2 a N x.left;
        have hN1 := Cauchy_iff_convergent._proof_3 a N hN0;
        have h1 := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N x.right hN0 hN1);
        have h2 :=
          Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
            (id
              (id
                (le_sSup
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                        (a.from N).inf))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).inf⟩)))));
        have h3 := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N x.right hN0 hN1);
        have h4 :=
          Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
            (id
              (id
                (sInf_le
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                        (a.from N).sup))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).sup⟩)))));
        have h1 := LE.le.trans h1 h2;
        have h4 := LE.le.trans h4 h3;
        Cauchy_iff_convergent._proof_7 a L_plus L_minus ε N h1 h4)
      (Classical.choose (h ε hε)) (Classical.choose_spec (h ε hε))hlow:0 < L_plus - L_minus⊢ L_plus = L_minush.inra:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hup:∀ ε > 0, L_plus - L_minus ≤ 2 * ε := 
  fun ε hε =>
    (fun N x =>
        have hN0 := Cauchy_iff_convergent._proof_2 a N x.left;
        have hN1 := Cauchy_iff_convergent._proof_3 a N hN0;
        have h1 := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N x.right hN0 hN1);
        have h2 :=
          Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
            (id
              (id
                (le_sSup
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                        (a.from N).inf))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).inf⟩)))));
        have h3 := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N x.right hN0 hN1);
        have h4 :=
          Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
            (id
              (id
                (sInf_le
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                        (a.from N).sup))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).sup⟩)))));
        have h1 := LE.le.trans h1 h2;
        have h4 := LE.le.trans h4 h3;
        Cauchy_iff_convergent._proof_7 a L_plus L_minus ε N h1 h4)
      (Classical.choose (h ε hε)) (Classical.choose_spec (h ε hε))hlow:0 = L_plus - L_minus⊢ L_plus = L_minus
  .h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hup:∀ ε > 0, L_plus - L_minus ≤ 2 * ε := 
  fun ε hε =>
    (fun N x =>
        have hN0 := Cauchy_iff_convergent._proof_2 a N x.left;
        have hN1 := Cauchy_iff_convergent._proof_3 a N hN0;
        have h1 := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N x.right hN0 hN1);
        have h2 :=
          Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
            (id
              (id
                (le_sSup
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                        (a.from N).inf))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).inf⟩)))));
        have h3 := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N x.right hN0 hN1);
        have h4 :=
          Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
            (id
              (id
                (sInf_le
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                        (a.from N).sup))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).sup⟩)))));
        have h1 := LE.le.trans h1 h2;
        have h4 := LE.le.trans h4 h3;
        Cauchy_iff_convergent._proof_7 a L_plus L_minus ε N h1 h4)
      (Classical.choose (h ε hε)) (Classical.choose_spec (h ε hε))hlow:0 < L_plus - L_minus⊢ L_plus = L_minus specialize hup ((L_plus - L_minus)/3) ?_h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hup:∀ ε > 0, L_plus - L_minus ≤ 2 * ε := 
  fun ε hε =>
    (fun N x =>
        have hN0 := Cauchy_iff_convergent._proof_2 a N x.left;
        have hN1 := Cauchy_iff_convergent._proof_3 a N hN0;
        have h1 := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N x.right hN0 hN1);
        have h2 :=
          Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
            (id
              (id
                (le_sSup
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                        (a.from N).inf))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).inf⟩)))));
        have h3 := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N x.right hN0 hN1);
        have h4 :=
          Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
            (id
              (id
                (sInf_le
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                        (a.from N).sup))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).sup⟩)))));
        have h1 := LE.le.trans h1 h2;
        have h4 := LE.le.trans h4 h3;
        Cauchy_iff_convergent._proof_7 a L_plus L_minus ε N h1 h4)
      (Classical.choose (h ε hε)) (Classical.choose_spec (h ε hε))hlow:0 < L_plus - L_minus⊢ (L_plus - L_minus) / 3 > 0h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hlow:0 < L_plus - L_minushup:L_plus - L_minus ≤ 2 * ((L_plus - L_minus) / 3)⊢ L_plus = L_minus <;>h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hup:∀ ε > 0, L_plus - L_minus ≤ 2 * ε := 
  fun ε hε =>
    (fun N x =>
        have hN0 := Cauchy_iff_convergent._proof_2 a N x.left;
        have hN1 := Cauchy_iff_convergent._proof_3 a N hN0;
        have h1 := inf_ge_lower (Cauchy_iff_convergent._proof_4 a ε N x.right hN0 hN1);
        have h2 :=
          Eq.mpr (id (congrArg (LE.le (a.from N).inf) (Eq.symm hL_minus)))
            (id
              (id
                (le_sSup
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).inf)))))
                        (a.from N).inf))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).inf⟩)))));
        have h3 := sup_le_upper (Cauchy_iff_convergent._proof_5 a ε N x.right hN0 hN1);
        have h4 :=
          Eq.mpr (id (congrFun' (congrArg LE.le (Eq.symm hL_plus)) (a.from N).sup))
            (id
              (id
                (sInf_le
                  (Eq.mpr
                    (id
                      (congrFun'
                        (congrArg Membership.mem
                          (congrArg setOf
                            (funext fun x =>
                              congrArg Exists
                                (funext fun N => congrFun' (congrArg And ge_iff_le._simp_1) (x = (a.from N).sup)))))
                        (a.from N).sup))
                    (Exists.intro N ⟨x.left, Eq.refl (a.from N).sup⟩)))));
        have h1 := LE.le.trans h1 h2;
        have h4 := LE.le.trans h4 h3;
        Cauchy_iff_convergent._proof_7 a L_plus L_minus ε N h1 h4)
      (Classical.choose (h ε hε)) (Classical.choose_spec (h ε hε))hlow:0 < L_plus - L_minus⊢ (L_plus - L_minus) / 3 > 0h.inla:Sequenceh:a.IsCauchyL_plus:ℝhL_plus:a.limsup = ↑L_plusL_minus:ℝhL_minus:a.liminf = ↑L_minushlow✝:0 ≤ L_plus - L_minus := 
  have this := liminf_le_limsup a;
  Cauchy_iff_convergent._proof_1 L_plus L_minus
    (Eq.mp (Eq.trans (congr (congrArg LE.le hL_minus) hL_plus) coe_le_coe_iff._simp_1) this)hlow:0 < L_plus - L_minushup:L_plus - L_minus ≤ 2 * ((L_plus - L_minus) / 3)⊢ L_plus = L_minus linarithAll goals completed! 🐙
  grindAll goals completed! 🐙

Exercise 6.4.6

theorem declaration uses `sorry`Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ ¬ (a:Sequence).sup < (b:Sequence).sup := by⊢ ∃ a b, (∀ (n : ℕ), a n < b n) ∧ ¬(↑a).sup < (↑b).sup
  sorryAll goals completed! 🐙

/- Exercise 6.4.7 -/
def declaration uses `sorry`Sequence.tendsTo_real_iff :
  Decidable (∀ (a:Sequence) (x:ℝ), a.TendsTo x ↔ a.abs.TendsTo x) := by⊢ Decidable (∀ (a : Sequence) (x : ℝ), a.TendsTo x ↔ a.abs.TendsTo x)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

This definition is needed for Exercises 6.4.8 and 6.4.9.

abbrev Sequence.ExtendedLimitPoint (a:Sequence) (x:EReal) : Prop := if x = ⊤ then ¬ a.BddAbove else if x = ⊥ then ¬ a.BddBelow else a.LimitPoint x.toReal

Exercise 6.4.8

theorem declaration uses `sorry`Sequence.extended_limit_point_of_limsup (a:Sequence) : a.ExtendedLimitPoint a.limsup := bya:Sequence⊢ a.ExtendedLimitPoint a.limsup sorryAll goals completed! 🐙

Exercise 6.4.8

theorem declaration uses `sorry`Sequence.extended_limit_point_of_liminf (a:Sequence) : a.ExtendedLimitPoint a.liminf := bya:Sequence⊢ a.ExtendedLimitPoint a.liminf sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.extended_limit_point_le_limsup {a:Sequence} {L:EReal} (h:a.ExtendedLimitPoint L): L ≤ a.limsup := bya:SequenceL:ERealh:a.ExtendedLimitPoint L⊢ L ≤ a.limsup sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.extended_limit_point_ge_liminf {a:Sequence} {L:EReal} (h:a.ExtendedLimitPoint L): L ≥ a.liminf := bya:SequenceL:ERealh:a.ExtendedLimitPoint L⊢ L ≥ a.liminf sorryAll goals completed! 🐙

Exercise 6.4.9

theorem declaration uses `sorry`Sequence.exists_three_limit_points : ∃ a:Sequence, ∀ L:EReal, a.ExtendedLimitPoint L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ := by⊢ ∃ a, ∀ (L : EReal), a.ExtendedLimitPoint L ↔ L = ⊥ ∨ L = 0 ∨ L = ⊤ sorryAll goals completed! 🐙

Exercise 6.4.10

theorem declaration uses `sorry`Sequence.limit_points_of_limit_points {a b:Sequence} {c:ℝ} (hab: ∀ n ≥ b.m, a.LimitPoint (b n)) (hbc: b.LimitPoint c) : a.LimitPoint c := bya:Sequenceb:Sequencec:ℝhab:∀ n ≥ b.m, a.LimitPoint (b.seq n)hbc:b.LimitPoint c⊢ a.LimitPoint c sorryAll goals completed! 🐙

end Chapter6