Analysis
5.1. Cauchy sequences

Imports

import Mathlib.Tactic
import Analysis.Section_4_3

set_option doc.verso.suggestions false

Analysis I, Section 5.1: Cauchy sequences

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:

Notion of a sequence of rationals
Notions of ε-steadiness, eventual ε-steadiness, and Cauchy sequences

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.1.1 (Sequence). To avoid some technicalities involving dependent types, we extend sequences by zero to the left of the starting point n₀.

@[ext]
structure Sequence where
  n₀ : ℤ
  seq : ℤ → ℚ
  vanish : ∀ n < n₀, seq n = 0

Sequences can be thought of as functions from ℤ to ℚ.

instance Sequence.instCoeFun : CoeFun Sequence (fun _ ↦ ℤ → ℚ) where
  coe := fun a ↦ a.seq

Functions from ℕ to ℚ can be thought of as sequences starting from 0; Sequence.ofNatFun performs this conversion.

The coe attribute allows the delaborator to print Sequence.ofNatFun f as ↑f, which is more concise; you may safely remove this if you prefer the more explicit notation.

@[coe]
def Sequence.ofNatFun (f : ℕ → ℚ) : Sequence where
    n₀ := 0
    seq n := if n ≥ 0 then f n.toNat else 0
    vanish := byf:ℕ → ℚ⊢ ∀ n < 0, (if n ≥ 0 then f n.toNat else 0) = 0 grindAll goals completed! 🐙

-- Notice how the delaborator prints this as `↑fun x ↦ ↑x ^ 2 : Sequence`.
↑fun x ↦ ↑x ^ 2 : Sequence#check Sequence.ofNatFun (· ^ 2)

If a : ℕ → ℚ is used in a context where a Sequence is expected, automatically coerce a to Sequence.ofNatFun a (which will be pretty-printed as ↑a).

instance : Coe (ℕ → ℚ) Sequence where
  coe := Sequence.ofNatFun

              abbrev Sequence.mk' (n₀:ℤ) (a: { n // n ≥ n₀ } → ℚ) : Sequence where
  n₀ := n₀
  seq n := if h : n ≥ n₀ then a ⟨n, h⟩ else 0
  vanish := byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ ∀ n < n₀, (if h : n ≥ n₀ then a ⟨n, h⟩ else 0) = 0 grindAll goals completed! 🐙lemma Sequence.eval_mk {n n₀:ℤ} (a: { n // n ≥ n₀ } → ℚ) (h: n ≥ n₀) :
    (Sequence.mk' n₀ a) n = a ⟨ n, h ⟩ := byn:ℤn₀:ℤa:{ n // n ≥ n₀ } → ℚh:n ≥ n₀⊢ (mk' n₀ a).seq n = a ⟨n, h⟩ grindAll goals completed! 🐙@[simp]
lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℚ) : (a:Sequence) n = a n := byn:ℕa:ℕ → ℚ⊢ (↑a).seq ↑n = a n norm_castAll goals completed! 🐙@[simp]
lemma Sequence.eval_coe_at_int (n:ℤ) (a: ℕ → ℚ) : (a:Sequence) n = if n ≥ 0 then a n.toNat else 0 := byn:ℤa:ℕ → ℚ⊢ (↑a).seq n = if n ≥ 0 then a n.toNat else 0 norm_castAll goals completed! 🐙@[simp]
lemma Sequence.n0_coe (a: ℕ → ℚ) : (a:Sequence).n₀ = 0 := bya:ℕ → ℚ⊢ (↑a).n₀ = 0 norm_castAll goals completed! 🐙

Example 5.1.2

abbrev Sequence.squares : Sequence := ((fun n:ℕ ↦ (n^2:ℚ)):Sequence)

/-- Example 5.1.2 -/
example (n:ℕ) : Sequence.squares n = n^2 := Sequence.eval_coe _ _

Example 5.1.2

abbrev Sequence.three : Sequence := ((fun (_:ℕ) ↦ (3:ℚ)):Sequence)

/-- Example 5.1.2 -/
example (n:ℕ) : Sequence.three n = 3 := Sequence.eval_coe _ (fun (_:ℕ) ↦ (3:ℚ))

Example 5.1.2

abbrev Sequence.squares_from_three : Sequence := mk' 3 (·^2)

/-- Example 5.1.2 -/
example (n:ℤ) (hn: n ≥ 3) : Sequence.squares_from_three n = n^2 := Sequence.eval_mk _ hn

-- need to temporarily leave the `Chapter5` namespace to introduce the following notation

end Chapter5

A slight generalization of Definition 5.1.3 - definition of ε-steadiness for a sequence with an arbitrary starting point a.n₀

abbrev Rat.Steady (ε: ℚ) (a: Chapter5.Sequence) : Prop :=
  ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a n) (a m)

lemma Rat.steady_def (ε: ℚ) (a: Chapter5.Sequence) :
  ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a n) (a m) := byε:ℚa:Chapter5.Sequence⊢ ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m) rflAll goals completed! 🐙

namespace Chapter5

Definition 5.1.3 - definition of ε-steadiness for a sequence starting at 0

lemma Rat.Steady.coe (ε : ℚ) (a:ℕ → ℚ) :
    ε.Steady a ↔ ∀ n m : ℕ, ε.Close (a n) (a m) := byε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m)
  constructormpε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m)mprε:ℚa:ℕ → ℚ⊢ (∀ (n m : ℕ), ε.Close (a n) (a m)) → ε.Steady ↑a
  ·mpε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m) intro h nmpε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕ⊢ ∀ (m : ℕ), ε.Close (a n) (a m) mmpε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ε.Close (a n) (a m); specialize h n ?_ m ?_mp.specialize_1ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀mp.specialize_2ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀mpε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) <;>mp.specialize_1ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀mp.specialize_2ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀mpε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) simp_allAll goals completed! 🐙
  intro h nmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤ⊢ n ≥ (↑a).n₀ → ∀ m ≥ (↑a).n₀, ε.Close ((↑a).seq n) ((↑a).seq m) hnmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤhn:n ≥ (↑a).n₀⊢ ∀ m ≥ (↑a).n₀, ε.Close ((↑a).seq n) ((↑a).seq m) mmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤhn:n ≥ (↑a).n₀m:ℤ⊢ m ≥ (↑a).n₀ → ε.Close ((↑a).seq n) ((↑a).seq m) hmmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤhn:n ≥ (↑a).n₀m:ℤhm:m ≥ (↑a).n₀⊢ ε.Close ((↑a).seq n) ((↑a).seq m)
  lift n to ℕ using hnmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)m:ℤhm:m ≥ (↑a).n₀n:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq m)
  lift m to ℕ using hmmprε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℕm:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)
  simp [h n m]All goals completed! 🐙

              /--
Not in textbook: the sequence 3, 3 ... is 1-steady.
Intended as a demonstration of {name}`Rat.Steady.coe`.
-/
example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := by⊢ Rat.Steady 1 ↑fun x ↦ 3
  simp [Rat.Steady.coe, Rat.Close]All goals completed! 🐙/--
{given -show}`hn : n ≥ 0, hm : m ≥ 0`
Compare: if you need to work with {name}`Rat.Steady` on the coercion directly, there will be side
conditions {lean}`hn : n ≥ 0` and {lean}`hm : m ≥ 0` that you will need to deal with.
-/
example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := by⊢ Rat.Steady 1 ↑fun x ↦ 3
  intro n _n:ℤa✝:n ≥ (↑fun x ↦ 3).n₀⊢ ∀ m ≥ (↑fun x ↦ 3).n₀, Rat.Close 1 ((↑fun x ↦ 3).seq n) ((↑fun x ↦ 3).seq m) mn:ℤa✝:n ≥ (↑fun x ↦ 3).n₀m:ℤ⊢ m ≥ (↑fun x ↦ 3).n₀ → Rat.Close 1 ((↑fun x ↦ 3).seq n) ((↑fun x ↦ 3).seq m) _n:ℤa✝¹:n ≥ (↑fun x ↦ 3).n₀m:ℤa✝:m ≥ (↑fun x ↦ 3).n₀⊢ Rat.Close 1 ((↑fun x ↦ 3).seq n) ((↑fun x ↦ 3).seq m); simp_all [Sequence.n0_coe, Sequence.eval_coe_at_int, Rat.Close]All goals completed! 🐙/--
Example 5.1.5: The sequence `1, 0, 1, 0, ...` is 1-steady.
-/
example : (1:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := by⊢ Rat.Steady 1 ↑fun n ↦ if Even n then 1 else 0
  rw [Rat.Steady.coe]⊢ ∀ (n m : ℕ), Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0)
  intro n mn:ℕm:ℕ⊢ Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0)
  -- Split into four cases based on whether n and m are even or odd
  -- In each case, we know the exact value of a n and a m
  split_ifsposn:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1negn:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0posn:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1negn:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 <;>posn:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1negn:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0posn:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1negn:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 simp [Rat.Close]All goals completed! 🐙/--
Example 5.1.5: The sequence `1, 0, 1, 0, ...` is not ½-steady.
-/
example : ¬ (0.5:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := by⊢ ¬Rat.Steady 0.5 ↑fun n ↦ if Even n then 1 else 0
  rw [Rat.Steady.coe]⊢ ¬∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0)
  by_contra hh:∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0)⊢ False; specialize h 0 1h:Rat.Close 0.5 (if Even 0 then 1 else 0) (if Even 1 then 1 else 0)⊢ False; simp [Rat.Close] at hh:1 ≤ 0.5⊢ False
  norm_num at hAll goals completed! 🐙/--
Example 5.1.5: The sequence 0.1, 0.01, 0.001, ... is 0.1-steady.
-/
example : (0.1:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := by⊢ Rat.Steady 0.1 ↑fun n ↦ 10 ^ (-↑n - 1)
  rw [Rat.Steady.coe]⊢ ∀ (n m : ℕ), Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1))
  intro n mn:ℕm:ℕ⊢ Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1)); unfold Rat.Closen:ℕm:ℕ⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1
  wlog h : m ≤ ninrn:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1
  ·inrn:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 specialize this m n (byn:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ n ≤ m linarithAll goals completed! 🐙); rwa [abs_sub_comm]inrn:ℕm:ℕh:¬m ≤ nthis:|10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1⊢ |10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1
  rw [abs_sub_comm, abs_of_nonneg]n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)
  .n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1 rw [show (0.1:ℚ) = (10:ℚ)^(-1:ℤ) - 0 by norm_num]n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 10 ^ (-1) - 0
    gcongrhab.han:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10hab.hmnn:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1hcdn:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) <;>hab.han:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10hab.hmnn:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1hcdn:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) try grindAll goals completed! 🐙
    positivityAll goals completed! 🐙
  linarith [show (10:ℚ) ^ (-(n:ℤ)-1) ≤ (10:ℚ) ^ (-(m:ℤ)-1) by⊢ Rat.Steady 0.1 ↑fun n ↦ 10 ^ (-↑n - 1) gcongrhan:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10; norm_numAll goals completed! 🐙]/--
Example 5.1.5: The sequence 0.1, 0.01, 0.001, ... is not 0.01-steady. Left as an exercise.
-/
declaration uses `sorry`example : ¬(0.01:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := by⊢ ¬Rat.Steady 1e-2 ↑fun n ↦ 10 ^ (-↑n - 1) sorryAll goals completed! 🐙/-- Example 5.1.5: The sequence 1, 2, 4, 8, ... is not ε-steady for any ε. Left as an exercise.
-/
declaration uses `sorry`example (ε:ℚ) : ¬ ε.Steady ((fun n:ℕ ↦ (2 ^ (n+1):ℚ) ):Sequence) := byε:ℚ⊢ ¬ε.Steady ↑fun n ↦ 2 ^ (n + 1) sorryAll goals completed! 🐙/-- Example 5.1.5:The sequence 2, 2, 2, ... is ε-steady for any ε > 0.
-/
example (ε:ℚ) (hε: ε>0) : ε.Steady ((fun _:ℕ ↦ (2:ℚ) ):Sequence) := byε:ℚhε:ε > 0⊢ ε.Steady ↑fun x ↦ 2
  rw [Rat.Steady.coe]ε:ℚhε:ε > 0⊢ ∀ (n m : ℕ), ε.Close 2 2; simp [Rat.Close]ε:ℚhε:ε > 0⊢ 0 ≤ ε; positivityAll goals completed! 🐙/--
The sequence 10, 0, 0, ... is 10-steady.
-/
example : (10:ℚ).Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := by⊢ Rat.Steady 10 ↑fun n ↦ if n = 0 then 10 else 0
  rw [Rat.Steady.coe]⊢ ∀ (n m : ℕ), Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0); intro n mn:ℕm:ℕ⊢ Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0)
  -- Split into 4 cases based on whether n and m are 0 or not
  split_ifsposn:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10negn:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0posn:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10negn:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 <;>posn:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10negn:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0posn:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10negn:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 simp [Rat.Close]All goals completed! 🐙/--
The sequence 10, 0, 0, ... is not ε-steady for any smaller value of ε.
-/
example (ε:ℚ) (hε:ε<10):  ¬ ε.Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := byε:ℚhε:ε < 10⊢ ¬ε.Steady ↑fun n ↦ if n = 0 then 10 else 0
  contrapose! hεε:ℚhε:ε.Steady ↑fun n ↦ if n = 0 then 10 else 0⊢ 10 ≤ ε; rw [Rat.Steady.coe] at hεε:ℚhε:∀ (n m : ℕ), ε.Close (if n = 0 then 10 else 0) (if m = 0 then 10 else 0)⊢ 10 ≤ ε; specialize hε 0 1ε:ℚhε:ε.Close (if 0 = 0 then 10 else 0) (if 1 = 0 then 10 else 0)⊢ 10 ≤ ε; simpa [Rat.Close] using hεAll goals completed! 🐙

Sequence.from starts a : Sequence from n₁. It is intended for use when n₁ ≥ n₀, but returns the "junk" value of the original sequence a otherwise.

abbrev Sequence.from (a:Sequence) (n₁:ℤ) : Sequence :=
  mk' (max a.n₀ n₁) (fun n ↦ a (n:ℤ))

lemma Sequence.from_eval (a:Sequence) {n₁ n:ℤ} (hn: n ≥ n₁) :
  (a.from n₁) n = a n := bya:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ (a.from n₁).seq n = a.seq n simp [hn]a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ n < a.n₀ → 0 = a.seq n; intro ha:Sequencen₁:ℤn:ℤhn:n ≥ n₁h:n < a.n₀⊢ 0 = a.seq n; exact (a.vanish _ h).symmAll goals completed! 🐙

end Chapter5

Definition 5.1.6 (Eventually ε-steady)

abbrev Rat.EventuallySteady (ε: ℚ) (a: Chapter5.Sequence) : Prop := ∃ N ≥ a.n₀, ε.Steady (a.from N)

lemma Rat.eventuallySteady_def (ε: ℚ) (a: Chapter5.Sequence) :
  ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N) := byε:ℚa:Chapter5.Sequence⊢ ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N) rflAll goals completed! 🐙

namespace Chapter5

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is not 0.1-steady

lemma Sequence.ex_5_1_7_a : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := by⊢ ¬Rat.Steady 0.1 ↑fun n ↦ (↑n + 1)⁻¹
  intro hh:Rat.Steady 0.1 ↑fun n ↦ (↑n + 1)⁻¹⊢ False; rw [Rat.Steady.coe] at hh:∀ (n m : ℕ), Rat.Close 0.1 (↑n + 1)⁻¹ (↑m + 1)⁻¹⊢ False; specialize h 0 2h:Rat.Close 0.1 (↑0 + 1)⁻¹ (↑2 + 1)⁻¹⊢ False; simp [Rat.Close] at hh:|1 - (2 + 1)⁻¹| ≤ 0.1⊢ False; norm_num at hAll goals completed! 🐙

Example 5.1.7: The sequence a_10, a_11, a_12, ... is 0.1-steady

lemma Sequence.ex_5_1_7_b : (0.1:ℚ).Steady (((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence).from 10) := by⊢ Rat.Steady 0.1 ((↑fun n ↦ (↑n + 1)⁻¹).from 10)
  rw [Rat.Steady]⊢ ∀ n ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀,
  ∀ m ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀,
    Rat.Close 0.1 (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq n) (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq m)
  intro n hnn:ℤhn:n ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀⊢ ∀ m ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀,
  Rat.Close 0.1 (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq n) (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq m) mn:ℤhn:n ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀m:ℤ⊢ m ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀ →
  Rat.Close 0.1 (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq n) (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq m) hmn:ℤhn:n ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀m:ℤhm:m ≥ ((↑fun n ↦ (↑n + 1)⁻¹).from 10).n₀⊢ Rat.Close 0.1 (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq n) (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq m); simp at hn hmn:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ Rat.Close 0.1 (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq n) (((↑fun n ↦ (↑n + 1)⁻¹).from 10).seq m)
  lift n to ℕ using (byn:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ 0 ≤ n omegaAll goals completed! 🐙)
  lift m to ℕ using (bym:ℤhm:10 ≤ mn:ℕhn:10 ≤ ↑n⊢ 0 ≤ m omegaAll goals completed! 🐙)
  simp_all [Rat.Close]n:ℕm:ℕhn:10 ≤ nhm:10 ≤ m⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1
  wlog h : m ≤ ninrn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1
  ·inrn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 specialize this m n _ _ _inr.specialize_1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ minr.specialize_2n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ ninr.specialize_3n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ minrn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 <;>inr.specialize_1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ minr.specialize_2n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ ninr.specialize_3n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ minrn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 try omegaAll goals completed! 🐙
    rwa [abs_sub_comm]inrn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 at this
  rw [abs_sub_comm]n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1
  have : ((n:ℚ) + 1)⁻¹ ≤ ((m:ℚ) + 1)⁻¹ := by⊢ Rat.Steady 0.1 ((↑fun n ↦ (↑n + 1)⁻¹).from 10) gcongrAll goals completed! 🐙
  rw [abs_of_nonneg (by linarith), show (0.1:ℚ) = (10:ℚ)⁻¹ - 0 by norm_num]n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑n + 1)⁻¹ ≤ (↑m + 1)⁻¹⊢ (↑m + 1)⁻¹ - (↑n + 1)⁻¹ ≤ 10⁻¹ - 0
  gcongrhab.hban:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑n + 1)⁻¹ ≤ (↑m + 1)⁻¹⊢ 10 ≤ ↑m + 1hcdn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑n + 1)⁻¹ ≤ (↑m + 1)⁻¹⊢ 0 ≤ (↑n + 1)⁻¹
  ·hab.hban:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑n + 1)⁻¹ ≤ (↑m + 1)⁻¹⊢ 10 ≤ ↑m + 1 norm_casthab.hban:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑n + 1)⁻¹ ≤ (↑m + 1)⁻¹⊢ 10 ≤ m + 1; omegaAll goals completed! 🐙
  positivityAll goals completed! 🐙

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is eventually 0.1-steady

lemma Sequence.ex_5_1_7_c : (0.1:ℚ).EventuallySteady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) :=
  ⟨10, by⊢ 10 ≥ (↑fun n ↦ (↑n + 1)⁻¹).n₀ simpAll goals completed! 🐙, ex_5_1_7_b⟩

Example 5.1.7

The sequence 10, 0, 0, ... is eventually ε-steady for every ε > 0. Left as an exercise.

lemma declaration uses `sorry`Sequence.ex_5_1_7_d {ε:ℚ} (hε:ε>0) :
    ε.EventuallySteady ((fun n:ℕ ↦ if n=0 then (10:ℚ) else (0:ℚ) ):Sequence) := byε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑fun n ↦ if n = 0 then 10 else 0 sorryAll goals completed! 🐙

abbrev Sequence.IsCauchy (a:Sequence) : Prop := ∀ ε > (0:ℚ), ε.EventuallySteady a

lemma Sequence.isCauchy_def (a:Sequence) :
  a.IsCauchy ↔ ∀ ε > (0:ℚ), ε.EventuallySteady a := bya:Sequence⊢ a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a rflAll goals completed! 🐙

Definition of Cauchy sequences, for a sequence starting at 0

lemma Sequence.IsCauchy.coe (a:ℕ → ℚ) :
    (a:Sequence).IsCauchy ↔ ∀ ε > (0:ℚ), ∃ N, ∀ j ≥ N, ∀ k ≥ N,
    Section_4_3.dist (a j) (a k) ≤ ε := bya:ℕ → ℚ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε
  constructormpa:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εmpra:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy <;>mpa:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εmpra:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy intro h εmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚ⊢ ε > 0 → ε.EventuallySteady ↑a hεmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑a
  ·mpa:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε choose N hN h' using h ε hεmpa:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (↑a).n₀h':ε.Steady ((↑a).from N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε
    lift N to ℕ using hNmpa:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε; use Nha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε
    intro j _ha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕa✝:j ≥ N⊢ ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε kha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕa✝:j ≥ Nk:ℕ⊢ k ≥ N → Section_4_3.dist (a j) (a k) ≤ ε _ha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ N⊢ Section_4_3.dist (a j) (a k) ≤ ε; simp [Rat.steady_def] at h'ha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
          (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε; specialize h' j _ k _h.specialize_1a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
          (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑jh.specialize_2a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
          (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑kha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0)
  (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε <;>h.specialize_1a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
          (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑jh.specialize_2a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ),
  ↑N ≤ n →
    ∀ (m : ℤ),
      ↑N ≤ m →
        ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
          (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑kha:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0)
  (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε try omegaAll goals completed! 🐙
    simp_allha:ℕ → ℚh:(↑a).IsCauchyε:ℚN:ℕj:ℕk:ℕhε:0 < εa✝¹:N ≤ ja✝:N ≤ kh':ε.Close (a j) (a k)⊢ Section_4_3.dist (a j) (a k) ≤ ε; exact h'All goals completed! 🐙
  choose N h' using h ε hεmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ ε.EventuallySteady ↑a
  refine ⟨ max N 0, bya:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ max (↑N) 0 ≥ (↑a).n₀ simpAll goals completed! 🐙, ?_ ⟩
  intro n hnmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).n₀⊢ ∀ m ≥ ((↑a).from (max (↑N) 0)).n₀, ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) mmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).n₀m:ℤ⊢ m ≥ ((↑a).from (max (↑N) 0)).n₀ → ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) hmmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).n₀m:ℤhm:m ≥ ((↑a).from (max (↑N) 0)).n₀⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m); simp at hn hmmpra:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)
  have npos : 0 ≤ n := ?_mpr.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)mpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n
  have mpos : 0 ≤ m := ?_mpr.refine_2.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ nmpos:0 ≤ m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)mpr.refine_2.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ 0 ≤ mmpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n
  lift n to ℕ using nposmpr.refine_2.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εm:ℤhm:↑N ≤ mmpos:0 ≤ mn:ℕhn:↑N ≤ ↑n⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq m)mpr.refine_2.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ 0 ≤ mmpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n
  lift m to ℕ using mposmpr.refine_2.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq ↑m)mpr.refine_2.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ 0 ≤ mmpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n
  simp [hn, hm]mpr.refine_2.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (a n) (a m)mpr.refine_2.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ 0 ≤ mmpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n; specialize h' n _ m _mpr.refine_2.refine_2.specialize_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ n ≥ Nmpr.refine_2.refine_2.specialize_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ m ≥ Nmpr.refine_2.refine_2a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑mh':Section_4_3.dist (a n) (a m) ≤ ε⊢ ε.Close (a n) (a m)mpr.refine_2.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ n⊢ 0 ≤ mmpr.refine_1a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n
  all_goals try omegaAll goals completed! 🐙
  norm_castAll goals completed! 🐙

lemma Sequence.IsCauchy.mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℚ) :
    (mk' n₀ a).IsCauchy ↔ ∀ ε > (0:ℚ), ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N,
    Section_4_3.dist (mk' n₀ a j) (mk' n₀ a k) ≤ ε := byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
  constructormpn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).IsCauchy → ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εmprn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy <;>mpn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).IsCauchy → ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εmprn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy intro h εmprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚ⊢ ε > 0 → ε.EventuallySteady (mk' n₀ a) hεmprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) <;>mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εmprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) choose N hN h' using h ε hεmprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ ε.EventuallySteady (mk' n₀ a)
  ·mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε refine ⟨ N, hN, ?_ ⟩mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; dsimp at hNmpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; intro j _mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤa✝:j ≥ N⊢ ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε kmpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤa✝:j ≥ Nk:ℤ⊢ k ≥ N → Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε _mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ N⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    simp only [Rat.Steady, show max n₀ N = N by omega] at h'mpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε
    specialize h' j _ k _mp.specialize_1n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nmp.specialize_2n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nmpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0)
  (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε <;>mp.specialize_1n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nmp.specialize_2n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N,
  ∀ m ≥ N,
    ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0)
      (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nmpn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0)
  (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε try omegaAll goals completed! 🐙
    simp_all [show n₀ ≤ j byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε omegaAll goals completed! 🐙, show n₀ ≤ k byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε omegaAll goals completed! 🐙]
    exact h'All goals completed! 🐙
  refine ⟨ max n₀ N, byn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ max n₀ N ≥ (mk' n₀ a).n₀ simpAll goals completed! 🐙, ?_ ⟩
  intro n _mprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn:ℤa✝:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀⊢ ∀ m ≥ ((mk' n₀ a).from (max n₀ N)).n₀, ε.Close (((mk' n₀ a).from (max n₀ N)).seq n) (((mk' n₀ a).from (max n₀ N)).seq m) mmprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn:ℤa✝:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤ⊢ m ≥ ((mk' n₀ a).from (max n₀ N)).n₀ → ε.Close (((mk' n₀ a).from (max n₀ N)).seq n) (((mk' n₀ a).from (max n₀ N)).seq m) _mprn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn:ℤa✝¹:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀⊢ ε.Close (((mk' n₀ a).from (max n₀ N)).seq n) (((mk' n₀ a).from (max n₀ N)).seq m); simp_allmprn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ),
  0 < ε →
    ∃ N,
      n₀ ≤ N ∧
        ∀ (j : ℤ),
          N ≤ j →
            ∀ (k : ℤ),
              N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ),
  N ≤ j →
    ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ ε.Close (if h : n₀ ≤ n then a ⟨n, ⋯⟩ else 0) (if h : n₀ ≤ m then a ⟨m, ⋯⟩ else 0)
  apply h' n _ mmprn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ),
  0 < ε →
    ∃ N,
      n₀ ≤ N ∧
        ∀ (j : ℤ),
          N ≤ j →
            ∀ (k : ℤ),
              N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ),
  N ≤ j →
    ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ),
  0 < ε →
    ∃ N,
      n₀ ≤ N ∧
        ∀ (j : ℤ),
          N ≤ j →
            ∀ (k : ℤ),
              N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ),
  N ≤ j →
    ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n <;>mprn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ),
  0 < ε →
    ∃ N,
      n₀ ≤ N ∧
        ∀ (j : ℤ),
          N ≤ j →
            ∀ (k : ℤ),
              N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ),
  N ≤ j →
    ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ),
  0 < ε →
    ∃ N,
      n₀ ≤ N ∧
        ∀ (j : ℤ),
          N ≤ j →
            ∀ (k : ℤ),
              N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ),
  N ≤ j →
    ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n omegaAll goals completed! 🐙

noncomputable def Sequence.sqrt_two : Sequence := (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ))

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem declaration uses `sorry`Sequence.ex_5_1_10_a : (1:ℚ).Steady sqrt_two := by⊢ Rat.Steady 1 sqrt_two sorryAll goals completed! 🐙

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem declaration uses `sorry`Sequence.ex_5_1_10_b : (0.1:ℚ).Steady (sqrt_two.from 1) := by⊢ Rat.Steady 0.1 (sqrt_two.from 1) sorryAll goals completed! 🐙

theorem declaration uses `sorry`Sequence.ex_5_1_10_c : (0.1:ℚ).EventuallySteady sqrt_two := by⊢ Rat.EventuallySteady 0.1 sqrt_two sorryAll goals completed! 🐙

Proposition 5.1.11. The harmonic sequence, defined as a₁ = 1, a₂ = 1/2, ... is a Cauchy sequence.

theorem Sequence.IsCauchy.harmonic : (mk' 1 (fun n ↦ (1:ℚ)/n)).IsCauchy := by⊢ (mk' 1 fun n ↦ 1 / ↑↑n).IsCauchy
  rw [IsCauchy.mk]⊢ ∀ ε > 0, ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε
  intro ε hεε:ℚhε:ε > 0⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε
  -- We go by reverse from the book - first choose N such that N > 1/ε
  obtain ⟨ N, hN : N > 1/ε ⟩ := exists_nat_gt (1 / ε)ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / ε⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε
  have hN' : N > 0 := by⊢ (mk' 1 fun n ↦ 1 / ↑↑n).IsCauchy
    observe : (1/ε) > 0ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis:0 < 1 / ε⊢ N > 0
    observe : (N:ℚ) > 0ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis✝:0 < 1 / εthis:0 < ↑N⊢ N > 0
    norm_cast at thisAll goals completed! 🐙
  refine ⟨ N, byε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0⊢ ↑N ≥ 1 norm_castAll goals completed! 🐙, ?_ ⟩
  intro j hjε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℤhj:j ≥ ↑N⊢ ∀ k ≥ ↑N, Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε kε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℤhj:j ≥ ↑Nk:ℤ⊢ k ≥ ↑N → Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε hkε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq k) ≤ ε
  lift j to ℕ using (byε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ 0 ≤ j linarithAll goals completed! 🐙)
  lift k to ℕ using (byε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0k:ℤhk:k ≥ ↑Nj:ℕhj:↑j ≥ ↑N⊢ 0 ≤ k linarithAll goals completed! 🐙)
  norm_cast at hj hkε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist ((mk' 1 fun n ↦ 1 / ↑↑n).seq ↑j) ((mk' 1 fun n ↦ 1 / ↑↑n).seq ↑k) ≤ ε
  simp [show j ≥ 1 by linarith, show k ≥ 1 by linarith]ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε

  have hdist : Section_4_3.dist ((1:ℚ)/j) ((1:ℚ)/k) ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n ↦ 1 / ↑↑n).IsCauchy
    rw [Section_4_3.dist_eq, abs_le']ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N
    /-
    We establish the following bounds:
    - 1/j ∈ [0, 1/N]
    - 1/k ∈ [0, 1/N]
    These imply that the distance between 1/j and 1/k is at most 1/N - when they are as "far apart" as possible.
    -/
    have : 1/j ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n ↦ 1 / ↑↑n).IsCauchy gcongrAll goals completed! 🐙
    observe : (0:ℚ) ≤ 1/jε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝:1 / ↑j ≤ 1 / ↑Nthis:0 ≤ 1 / ↑j⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N
    have : 1/k ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n ↦ 1 / ↑↑n).IsCauchy gcongrAll goals completed! 🐙
    observe : (0:ℚ) ≤ 1/kε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':N > 0j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝²:1 / ↑j ≤ 1 / ↑Nthis✝¹:0 ≤ 1 / ↑jthis✝:1 / ↑k ≤ 1 / ↑Nthis:0 ≤ 1 / ↑k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N
    grindAll goals completed! 🐙
  simp at *ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε; apply hdist.transε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ (↑N)⁻¹ ≤ ε
  rw [inv_le_comm₀]ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nhaε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nhbε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε <;>ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nhaε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nhbε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε try positivityAll goals completed! 🐙
  orderAll goals completed! 🐙

abbrev BoundedBy {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : Prop := ∀ i, |a i| ≤ M

Definition 5.1.12 (bounded sequences). Here we start sequences from 0 rather than 1 to align better with Mathlib conventions.

lemma boundedBy_def {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : BoundedBy a M ↔ ∀ i, |a i| ≤ M := byn:ℕa:Fin n → ℚM:ℚ⊢ BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M rflAll goals completed! 🐙

abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop := ∀ n, |a n| ≤ M

Definition 5.1.12 (bounded sequences)

lemma Sequence.boundedBy_def (a:Sequence) (M:ℚ) : a.BoundedBy M ↔ ∀ n, |a n| ≤ M := bya:SequenceM:ℚ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M rflAll goals completed! 🐙

abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

Definition 5.1.12 (bounded sequences)

lemma Sequence.isBounded_def (a:Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M := bya:Sequence⊢ a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M rflAll goals completed! 🐙

              /-- Example 5.1.13 -/
example : BoundedBy ![1,-2,3,-4] 4 := by⊢ BoundedBy ![1, -2, 3, -4] 4 intro ii:Fin (Nat.succ 0).succ.succ.succ⊢ |![1, -2, 3, -4] i| ≤ 4; fin_cases i«0»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨0, ⋯⟩)| ≤ 4«1»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ 4«2»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨2, ⋯⟩)| ≤ 4«3»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨3, ⋯⟩)| ≤ 4 <;>«0»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨0, ⋯⟩)| ≤ 4«1»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ 4«2»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨2, ⋯⟩)| ≤ 4«3»⊢ |![1, -2, 3, -4] ((fun i ↦ i) ⟨3, ⋯⟩)| ≤ 4 norm_numAll goals completed! 🐙/-- Example 5.1.13 -/
declaration uses `sorry`example : ¬((fun n:ℕ ↦ (-1)^n * (n+1:ℚ)):Sequence).IsBounded := by⊢ ¬(↑fun n ↦ (-1) ^ n * (↑n + 1)).IsBounded sorryAll goals completed! 🐙/-- Example 5.1.13 -/
example : ((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsBounded := by⊢ (↑fun n ↦ (-1) ^ n).IsBounded
  refine ⟨ 1, by⊢ 1 ≥ 0 norm_numAll goals completed! 🐙, ?_ ⟩; intro ii:ℤ⊢ |(↑fun n ↦ (-1) ^ n).seq i| ≤ 1; by_cases h: 0 ≤ iposi:ℤh:0 ≤ i⊢ |(↑fun n ↦ (-1) ^ n).seq i| ≤ 1negi:ℤh:¬0 ≤ i⊢ |(↑fun n ↦ (-1) ^ n).seq i| ≤ 1 <;>posi:ℤh:0 ≤ i⊢ |(↑fun n ↦ (-1) ^ n).seq i| ≤ 1negi:ℤh:¬0 ≤ i⊢ |(↑fun n ↦ (-1) ^ n).seq i| ≤ 1 simp [h]All goals completed! 🐙/-- Example 5.1.13 -/
example : ¬((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsCauchy := by⊢ ¬(↑fun n ↦ (-1) ^ n).IsCauchy
  rw [Sequence.IsCauchy.coe]⊢ ¬∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε
  by_contra hh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ False; specialize h (1/2 : ℚ) (byh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ 1 / 2 > 0 norm_numAll goals completed! 🐙)
  choose N h using hN:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ False; specialize h N _ (N+1) _specialize_1N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ Nspecialize_2N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False <;>specialize_1N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ Nspecialize_2N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False try omegaN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False
  by_cases h': Even NposN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ FalsenegN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even N⊢ False
  ·posN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ False simp [h'.neg_one_pow, (h'.add_one).neg_one_pow, Section_4_3.dist] at hposN:ℕh':Even Nh:|1 + 1| ≤ 2⁻¹⊢ False
    norm_num at hAll goals completed! 🐙
  observe h₁: Odd NnegN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd N⊢ False
  observe h₂: Even (N+1)negN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd Nh₂:Even (N + 1)⊢ False
  simp [h₁.neg_one_pow, h₂.neg_one_pow, Section_4_3.dist] at hnegN:ℕh':¬Even Nh₁:Odd Nh₂:Even (N + 1)h:|-1 - 1| ≤ 2⁻¹⊢ False
  norm_num at hAll goals completed! 🐙

Lemma 5.1.14

lemma IsBounded.finite {n:ℕ} (a: Fin n → ℚ) : ∃ M ≥ 0,  BoundedBy a M := byn:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M
  -- this proof is written to follow the structure of the original text.
  induction' n with n hnzeroa:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a Msuccn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚ⊢ ∃ M ≥ 0, BoundedBy a M
  .zeroa:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a M use 0ha:Fin 0 → ℚ⊢ 0 ≥ 0 ∧ BoundedBy a 0; simpAll goals completed! 🐙
  set a' : Fin n → ℚ := fun m ↦ a m.castSuccsuccn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSucc⊢ ∃ M ≥ 0, BoundedBy a M
  choose M hpos hM using hn a'succn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' M⊢ ∃ M ≥ 0, BoundedBy a M
  have h1 : BoundedBy a' (M + |a (Fin.ofNat _ n)|) := fun m ↦ (hM m).trans (byn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mm:Fin n⊢ M ≤ M + |a (Fin.ofNat (n + 1) n)| simpAll goals completed! 🐙)
  have h2 : |a (Fin.ofNat _ n)| ≤ M + |a (Fin.ofNat _ n)| := byn:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M simp [hpos]All goals completed! 🐙
  refine ⟨ M + |a (Fin.ofNat _ n)|, byn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|⊢ M + |a (Fin.ofNat (n + 1) n)| ≥ 0 positivityAll goals completed! 🐙, ?_ ⟩
  intro msuccn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|m:Fin (n + 1)⊢ |a m| ≤ M + |a (Fin.ofNat (n + 1) n)|; obtain ⟨ j, rfl ⟩ | rfl := Fin.eq_castSucc_or_eq_last msucc.inln:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)|succ.inrn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|⊢ |a (Fin.last n)| ≤ M + |a (Fin.ofNat (n + 1) n)|
  .succ.inln:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)| grindAll goals completed! 🐙
  convert h2h.e'_3.h.e'_4.h.e'_1n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m ↦ a m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a (Fin.ofNat (n + 1) n)|)h2:|a (Fin.ofNat (n + 1) n)| ≤ M + |a (Fin.ofNat (n + 1) n)|⊢ Fin.last n = Fin.ofNat (n + 1) n; simpAll goals completed! 🐙

Lemma 5.1.15 (Cauchy sequences are bounded) / Exercise 5.1.1

lemma declaration uses `sorry`Sequence.isBounded_of_isCauchy {a:Sequence} (h: a.IsCauchy) : a.IsBounded := bya:Sequenceh:a.IsCauchy⊢ a.IsBounded
  sorryAll goals completed! 🐙

Exercise 5.1.2

theorem declaration uses `sorry`Sequence.isBounded_add {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded):
    (a + b:Sequence).IsBounded := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a + b)).IsBounded sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Sequence.isBounded_sub {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded):
    (a - b:Sequence).IsBounded := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a - b)).IsBounded sorryAll goals completed! 🐙theorem declaration uses `sorry`Sequence.isBounded_mul {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded):
    (a * b:Sequence).IsBounded := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a * b)).IsBounded sorryAll goals completed! 🐙end Chapter5