Analysis I, Section 5.3

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 formal limit of a Cauchy sequence
Construction of a real number type Chapter5.Real
Basic arithmetic operations and properties

namespace Chapter5

A class of Cauchy sequences that start at zero

@[ext]
class CauchySequence extends Sequence where
  zero : n₀ = 0
  cauchy : toSequence.isCauchy

theorem CauchySequence.ext' {a b: CauchySequence} (h: a.seq = b.seq) : a = b := bya:CauchySequenceb:CauchySequenceh:toSequence.seq = toSequence.seq⊢ a = b
  apply CauchySequence.extn₀a:CauchySequenceb:CauchySequenceh:toSequence.seq = toSequence.seq⊢ toSequence.n₀ = toSequence.n₀seqa:CauchySequenceb:CauchySequenceh:toSequence.seq = toSequence.seq⊢ toSequence.seq = toSequence.seq
  .n₀a:CauchySequenceb:CauchySequenceh:toSequence.seq = toSequence.seq⊢ toSequence.n₀ = toSequence.n₀ rw [a.zero, b.zero]All goals completed! 🐙
  exact hAll goals completed! 🐙

A sequence starting at zero that is Cauchy, can be viewed as a Cauchy sequence.

abbrev CauchySequence.mk' {a:ℕ → ℚ} (ha: (a:Sequence).isCauchy) : CauchySequence where
  n₀ := 0
  seq := (a:Sequence).seq
  vanish := bya:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∀ n < 0, (fun n => if n ≥ 0 then a n.toNat else 0) n = 0
    intro n hna:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℤhn:n < 0⊢ (fun n => if n ≥ 0 then a n.toNat else 0) n = 0
    exact (a:Sequence).vanish n hnAll goals completed! 🐙
  zero := rfl
  cauchy := ha

@[simp]
theorem CauchySequence.coe_eq {a:ℕ → ℚ} (ha: (a:Sequence).isCauchy) : (mk' ha).toSequence = (a:Sequence) := bya:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ toSequence = { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } rflAll goals completed! 🐙

instance CauchySequence.instCoeFun : CoeFun CauchySequence (fun _ ↦ ℕ → ℚ) where
  coe := fun a n ↦ a.toSequence (n:ℤ)

@[simp]
theorem CauchySequence.coe_to_sequence (a: CauchySequence) : ((a:ℕ → ℚ):Sequence) = a.toSequence := bya:CauchySequence⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ } = toSequence
  apply Sequence.extn₀a:CauchySequence⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.n₀ = toSequence.n₀seqa:CauchySequence⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.seq = toSequence.seq
  .n₀a:CauchySequence⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.n₀ = toSequence.n₀ rw [a.zero]All goals completed! 🐙
  ext nseq.ha:CauchySequencen:ℤ⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.seq n =
  toSequence.seq n
  by_cases h:n ≥ 0posa:CauchySequencen:ℤh:n ≥ 0⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.seq n =
  toSequence.seq nnega:CauchySequencen:ℤh:¬n ≥ 0⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => toSequence.seq ↑n) n.toNat else 0, vanish := ⋯ }.seq n =
  toSequence.seq n
  all_goals simp [h]nega:CauchySequencen:ℤh:¬n ≥ 0⊢ 0 = toSequence.seq n
  rw [a.vanish]neg.aa:CauchySequencen:ℤh:¬n ≥ 0⊢ n < toSequence.n₀
  rw [a.zero]neg.aa:CauchySequencen:ℤh:¬n ≥ 0⊢ n < 0
  exact lt_of_not_ge hAll goals completed! 🐙

@[simp]
theorem CauchySequence.coe_coe {a:ℕ → ℚ} (ha: (a:Sequence).isCauchy) : mk' ha = a := bya:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ (fun n => toSequence.seq ↑n) = a rflAll goals completed! 🐙

Proposition 5.3.3 / Exercise 5.3.1

theorem declaration uses 'sorry'Sequence.equiv_trans {a b c:ℕ → ℚ} (hab: Sequence.equiv a b) (hbc: Sequence.equiv b c) :
  Sequence.equiv a c := bya:ℕ → ℚb:ℕ → ℚc:ℕ → ℚhab:equiv a bhbc:equiv b c⊢ equiv a c sorryAll goals completed! 🐙

Proposition 5.3.3 / Exercise 5.3.1

instance declaration uses 'sorry'CauchySequence.instSetoid : Setoid CauchySequence where
  r := fun a b ↦ Sequence.equiv a b
  iseqv := {
     refl := sorry
     symm := sorry
     trans := sorry
  }

theorem CauchySequence.equiv_iff (a b: CauchySequence) : a ≈ b ↔ Sequence.equiv a b := bya:CauchySequenceb:CauchySequence⊢ a ≈ b ↔ Sequence.equiv (fun n => toSequence.seq ↑n) fun n => toSequence.seq ↑n rflAll goals completed! 🐙

Every constant sequence is Cauchy

theorem declaration uses 'sorry'Sequence.isCauchy_of_const (a:ℚ) : ((fun n:ℕ ↦ a):Sequence).isCauchy := bya:ℚ⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => a) n.toNat else 0, vanish := ⋯ }.isCauchy sorryAll goals completed! 🐙

instance CauchySequence.instZero : Zero CauchySequence where
  zero := CauchySequence.mk' (a := fun _: ℕ ↦ 0) (Sequence.isCauchy_of_const (0:ℚ))

abbrev Real := Quotient CauchySequence.instSetoid

open Classical in
/-- It is convenient in Lean to assign the "dummy" value of 0 to `LIM a` when `a` is not Cauchy.  This requires Classical logic, because the property of being Cauchy is not computable or decidable.  -/
noncomputable abbrev LIM (a:ℕ → ℚ) : Real := Quotient.mk _ (if h : (a:Sequence).isCauchy then CauchySequence.mk' h else (0:CauchySequence))

theorem LIM_def {a:ℕ → ℚ} (ha: (a:Sequence).isCauchy) : LIM a = Quotient.mk _ (CauchySequence.mk' ha) := bya:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a = ⟦CauchySequence.mk' ha⟧
  rw [LIM, dif_pos ha]All goals completed! 🐙

Definition 5.3.1 (Real numbers)

theorem Real.eq_lim (x:Real) : ∃ (a:ℕ → ℚ), (a:Sequence).isCauchy ∧ x = LIM a := byx:Real⊢ ∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = LIM a
  -- I had a lot of trouble with this proof; perhaps there is a more idiomatic way to proceed
  apply Quot.ind _ xx:Real⊢ ∀ (a : CauchySequence),
  ∃ a_1,
    { n₀ := 0, seq := fun n => if n ≥ 0 then a_1 n.toNat else 0, vanish := ⋯ }.isCauchy ∧
      Quot.mk (⇑CauchySequence.instSetoid) a = LIM a_1; intro ax:Reala:CauchySequence⊢ ∃ a_1,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a_1 n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    Quot.mk (⇑CauchySequence.instSetoid) a = LIM a_1
  set a' : ℕ → ℚ := (a:ℕ → ℚ)x:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑n⊢ ∃ a_1,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a_1 n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    Quot.mk (⇑CauchySequence.instSetoid) a = LIM a_1; use a'hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑n⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.isCauchy ∧
  Quot.mk (⇑CauchySequence.instSetoid) a = LIM a'
  set s : Sequence := (a':Sequence)hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }⊢ s.isCauchy ∧ Quot.mk (⇑CauchySequence.instSetoid) a = LIM a'
  have : s = a.toSequence := CauchySequence.coe_to_sequence ahx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ s.isCauchy ∧ Quot.mk (⇑CauchySequence.instSetoid) a = LIM a'
  rw [this]hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ CauchySequence.toSequence.isCauchy ∧ Quot.mk (⇑CauchySequence.instSetoid) a = LIM a'
  refine ⟨ a.cauchy, ?_ ⟩hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ Quot.mk (⇑CauchySequence.instSetoid) a = LIM a'
  congrh.e_ax:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ a =
  if h : { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.isCauchy then CauchySequence.mk' h
  else 0
  convert (dif_pos a.cauchy).symm with nh.e'_2x:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ a = CauchySequence.mk' ⋯h.e_a.convert_1x:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ Decidable CauchySequence.toSequence.isCauchy
  .h.e'_2x:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ a = CauchySequence.mk' ⋯ apply CauchySequence.ext'h.e'_2.hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ CauchySequence.toSequence.seq = CauchySequence.toSequence.seq
    change a.seq = s.seqh.e'_2.hx:Reala:CauchySequencea':ℕ → ℚ := fun n => CauchySequence.toSequence.seq ↑ns:Sequence := { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }this:s = CauchySequence.toSequence⊢ CauchySequence.toSequence.seq = s.seq
    rw [this]All goals completed! 🐙
  classical
  exact Classical.propDecidable _All goals completed! 🐙

Definition 5.3.1 (Real numbers)

theorem Real.LIM_eq_LIM {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
  LIM a = LIM b ↔ Sequence.equiv a b := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a = LIM b ↔ Sequence.equiv a b
  constructormpa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a = LIM b → Sequence.equiv a bmpra:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ Sequence.equiv a b → LIM a = LIM b
  .mpa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a = LIM b → Sequence.equiv a b intro hmpa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:LIM a = LIM b⊢ Sequence.equiv a b
    replace h := Quotient.exact hmpa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:(if h : { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy then CauchySequence.mk' h
  else 0) ≈
  if h : { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy then CauchySequence.mk' h
  else 0⊢ Sequence.equiv a b
    rwa [dif_pos ha, dif_pos hb, CauchySequence.equiv_iff]mpa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:Sequence.equiv (fun n => CauchySequence.toSequence.seq ↑n) fun n => CauchySequence.toSequence.seq ↑n⊢ Sequence.equiv a b at h
  intro hmpra:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:Sequence.equiv a b⊢ LIM a = LIM b
  apply Quotient.soundmpr.aa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:Sequence.equiv a b⊢ (if h : { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy then CauchySequence.mk' h
  else 0) ≈
  if h : { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy then CauchySequence.mk' h
  else 0
  rwa [dif_pos ha, dif_pos hb, CauchySequence.equiv_iff]mpr.aa:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyh:Sequence.equiv a b⊢ Sequence.equiv (fun n => CauchySequence.toSequence.seq ↑n) fun n => CauchySequence.toSequence.seq ↑n

Lemma 5.3.6 (Sum of Cauchy sequences is Cauchy)

theorem Sequence.add_cauchy {a b:ℕ → ℚ}  (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) : (a + b:Sequence).isCauchy := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy
  -- This proof is written to follow the structure of the original text.
  rw [isCauchy_def] at ha hb ⊢a:ℕ → ℚb:ℕ → ℚha:∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }hb:∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }⊢ ∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  intro ε hεa:ℕ → ℚb:ℕ → ℚha:∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }hb:∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }ε:ℚhε:ε > 0⊢ ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  have : ε/2 > 0 := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy exact half_pos hεAll goals completed! 🐙
  replace ha := ha (ε/2) thisa:ℕ → ℚb:ℕ → ℚhb:∀ ε > 0, ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }ε:ℚhε:ε > 0this:ε / 2 > 0ha:(ε / 2).eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }⊢ ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  replace hb := hb (ε/2) thisa:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0ha:(ε / 2).eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }hb:(ε / 2).eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }⊢ ε.eventuallySteady { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  rw [Rat.eventuallySteady_def] at ha hb ⊢a:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0ha:∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.n₀,
  (ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)hb:∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.n₀,
  (ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.from N)⊢ ∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.n₀,
  ε.steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
  obtain ⟨ N, hN, hha ⟩ := haintro.introa:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0hb:∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.n₀,
  (ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.from N)N:ℤhN:N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.n₀hha:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)⊢ ∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.n₀,
  ε.steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
  obtain ⟨ M, hM, hhb ⟩ := hbintro.intro.intro.introa:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤhN:N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.n₀hha:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)M:ℤhM:M ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.n₀hhb:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.from M)⊢ ∃ N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.n₀,
  ε.steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
  use max N Mha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤhN:N ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.n₀hha:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)M:ℤhM:M ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.n₀hhb:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.from M)⊢ max N M ≥ { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.n₀ ∧
  ε.steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from (max N M))
  simp at hN hM ⊢ha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤhha:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)M:ℤhhb:(ε / 2).steady ({ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.from M)hN:0 ≤ NhM:0 ≤ M⊢ (0 ≤ N ∨ 0 ≤ M) ∧
  ε.steady ({ n₀ := 0, seq := fun n => if 0 ≤ n then a n.toNat + b n.toNat else 0, vanish := ⋯ }.from (max N M))
  simp [hN, Rat.steady_def'] at hha hhb ⊢ha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mhha:∀ (n m : ℤ),
  N ≤ n →
    N ≤ m →
      (ε / 2).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)hhb:∀ (n m : ℤ),
  0 ≤ n →
    M ≤ n →
      0 ≤ m →
        M ≤ m →
          (ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
            (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)⊢ ∀ (n m : ℤ),
  N ≤ n →
    M ≤ n →
      N ≤ m →
        M ≤ m →
          ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
            (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  intro n m hnN hnM hmN hmMha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mhha:∀ (n m : ℤ),
  N ≤ n →
    N ≤ m →
      (ε / 2).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)hhb:∀ (n m : ℤ),
  0 ≤ n →
    M ≤ n →
      0 ≤ m →
        M ≤ m →
          (ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
            (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)n:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ m⊢ ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  have hn := hN.trans hnNha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mhha:∀ (n m : ℤ),
  N ≤ n →
    N ≤ m →
      (ε / 2).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)hhb:∀ (n m : ℤ),
  0 ≤ n →
    M ≤ n →
      0 ≤ m →
        M ≤ m →
          (ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
            (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)n:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ n⊢ ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  have hm := hM.trans hmMha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mhha:∀ (n m : ℤ),
  N ≤ n →
    N ≤ m →
      (ε / 2).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)hhb:∀ (n m : ℤ),
  0 ≤ n →
    M ≤ n →
      0 ≤ m →
        M ≤ m →
          (ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
            (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)n:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ nhm:0 ≤ m⊢ ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  replace hha := hha n m hnN hmNha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mhhb:∀ (n m : ℤ),
  0 ≤ n →
    M ≤ n →
      0 ≤ m →
        M ≤ m →
          (ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
            (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)n:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ nhm:0 ≤ mhha:(ε / 2).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)⊢ ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  replace hhb := hhb n m hn hnM hm hmMha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mn:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ nhm:0 ≤ mhha:(ε / 2).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)hhb:(ε / 2).close (if 0 ≤ n ∧ M ≤ n then if 0 ≤ n then b n.toNat else 0 else 0)
  (if 0 ≤ m ∧ M ≤ m then if 0 ≤ m then b m.toNat else 0 else 0)⊢ ε.close (if N ≤ n ∧ M ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if N ≤ m ∧ M ≤ m then if 0 ≤ m then a m.toNat + b m.toNat else 0 else 0)
  simp [hn, hm, hnN, hnM, hmN, hmM] at hha hhb ⊢ha:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mn:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ nhm:0 ≤ mhha:(ε / 2).close (a n.toNat) (a m.toNat)hhb:(ε / 2).close (b n.toNat) (b m.toNat)⊢ ε.close (a n.toNat + b n.toNat) (a m.toNat + b m.toNat)
  convert Section_4_3.add_close hha hhbh.e'_1a:ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0this:ε / 2 > 0N:ℤM:ℤhN:0 ≤ NhM:0 ≤ Mn:ℤm:ℤhnN:N ≤ nhnM:M ≤ nhmN:N ≤ mhmM:M ≤ mhn:0 ≤ nhm:0 ≤ mhha:(ε / 2).close (a n.toNat) (a m.toNat)hhb:(ε / 2).close (b n.toNat) (b m.toNat)⊢ ε = ε / 2 + ε / 2
  ringAll goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv_left {a a':ℕ → ℚ} (b:ℕ → ℚ) (haa': Sequence.equiv a a') :
  Sequence.equiv (a + b) (a' + b) := bya:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':equiv a a'⊢ equiv (a + b) (a' + b)
  -- This proof is written to follow the structure of the original text.
  rw [equiv_def] at haa' ⊢a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':∀ ε > 0,
  ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
    { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }⊢ ∀ ε > 0,
  ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
    { n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }
  intro ε hεa:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':∀ ε > 0,
  ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
    { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }ε:ℚhε:ε > 0⊢ ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }
  replace haa' := haa' ε hεa:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0haa':ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }⊢ ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }
  rw [Rat.eventually_close_def] at haa' ⊢a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0haa':∃ N,
  ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)
    ({ n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.from N)⊢ ∃ N,
  ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
    ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }.from N)
  obtain ⟨ N, haa' ⟩ := haa'introa:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤhaa':ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)
  ({ n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.from N)⊢ ∃ N,
  ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
    ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }.from N)
  use Nha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤhaa':ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N)
  ({ n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.from N)⊢ ε.close_seq ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N)
  ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }.from N)
  rw [Rat.close_seq_def] at haa' ⊢ha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤhaa':∀ n ≥ ({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N).n₀,
  n ≥ ({ n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.from N).n₀ →
    ε.close (({ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.from N).seq n)
      (({ n₀ := 0, seq := fun n => if n ≥ 0 then a' n.toNat else 0, vanish := ⋯ }.from N).seq n)⊢ ∀ n ≥ ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N).n₀,
  n ≥ ({ n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }.from N).n₀ →
    ε.close (({ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.from N).seq n)
      (({ n₀ := 0, seq := fun n => if n ≥ 0 then (a' + b) n.toNat else 0, vanish := ⋯ }.from N).seq n)
  simp at haa' ⊢ha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤhaa':∀ (n : ℤ),
  0 ≤ n →
    N ≤ n →
      0 ≤ n →
        N ≤ n →
          ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)⊢ ∀ (n : ℤ),
  0 ≤ n →
    N ≤ n →
      0 ≤ n →
        N ≤ n →
          ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
            (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat + b n.toNat else 0 else 0)
  intro n hn hN _ _ha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤhaa':∀ (n : ℤ),
  0 ≤ n →
    N ≤ n →
      0 ≤ n →
        N ≤ n →
          ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
            (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)n:ℤhn:0 ≤ nhN:N ≤ na✝¹:0 ≤ na✝:N ≤ n⊢ ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat + b n.toNat else 0 else 0)
  replace haa' := haa' n hn hN hn hNha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤn:ℤhn:0 ≤ nhN:N ≤ na✝¹:0 ≤ na✝:N ≤ nhaa':ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0)
  (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat else 0 else 0)⊢ ε.close (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a n.toNat + b n.toNat else 0 else 0)
  (if 0 ≤ n ∧ N ≤ n then if 0 ≤ n then a' n.toNat + b n.toNat else 0 else 0)
  simp [hn, hN] at haa' ⊢ha:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤn:ℤhn:0 ≤ nhN:N ≤ na✝¹:0 ≤ na✝:N ≤ nhaa':ε.close (a n.toNat) (a' n.toNat)⊢ ε.close (a n.toNat + b n.toNat) (a' n.toNat + b n.toNat)
  convert Section_4_3.add_close haa' (Section_4_3.close_refl (b n.toNat))h.e'_1a:ℕ → ℚa':ℕ → ℚb:ℕ → ℚε:ℚhε:ε > 0N:ℤn:ℤhn:0 ≤ nhN:N ≤ na✝¹:0 ≤ na✝:N ≤ nhaa':ε.close (a n.toNat) (a' n.toNat)⊢ ε = ε + 0
  simpAll goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv_right {b b':ℕ → ℚ} (a:ℕ → ℚ) (hbb': Sequence.equiv b b') :
  Sequence.equiv (a + b) (a + b') := byb:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':equiv b b'⊢ equiv (a + b) (a + b')
  simp_rw [add_comm]b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':equiv b b'⊢ equiv (b + a) (b' + a)
  exact add_equiv_left a hbb'All goals completed! 🐙

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Sequence.add_equiv {a b a' b':ℕ → ℚ} (haa': Sequence.equiv a a') (hbb': Sequence.equiv b b') :
  Sequence.equiv (a + b) (a' + b') := equiv_trans (add_equiv_left b haa') (add_equiv_right a' hbb')

Definition 5.3.4 (Addition of reals)

noncomputable instance Real.add_inst : Add Real where
  add := fun x y ↦
    Quotient.liftOn₂ x y (fun a b ↦ LIM (a + b)) (byx:Realy:Real⊢ ∀ (a₁ b₁ a₂ b₂ : CauchySequence),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)) a₁ b₁ =
        (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)) a₂ b₂
      intro a b a' b' haa' hbb'x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)) a b =
  (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)) a' b'
      change LIM ((a:ℕ → ℚ) + (b:ℕ → ℚ)) = LIM ((a':ℕ → ℚ) + (b':ℕ → ℚ))x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n) =
  LIM ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)
      rw [LIM_eq_LIM]x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.equiv ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)
  ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0,
    seq := fun n =>
      if n ≥ 0 then ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n) n.toNat
      else 0,
    vanish := ⋯ }.isCauchyhbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0,
    seq := fun n =>
      if n ≥ 0 then ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n) n.toNat
      else 0,
    vanish := ⋯ }.isCauchy
      .x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.equiv ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n)
  ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n) exact Sequence.add_equiv haa' hbb'All goals completed! 🐙
      all_goals apply Sequence.add_cauchyhb.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then CauchySequence.toSequence.seq ↑n.toNat else 0, vanish := ⋯ }.isCauchyhb.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then CauchySequence.toSequence.seq ↑n.toNat else 0, vanish := ⋯ }.isCauchy
      all_goals rw [CauchySequence.coe_to_sequence]hb.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy
      .ha.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact a.cauchyAll goals completed! 🐙
      .ha.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact b.cauchyAll goals completed! 🐙
      .hb.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact a'.cauchyAll goals completed! 🐙
      exact b'.cauchyAll goals completed! 🐙
      )

Definition 5.3.4 (Addition of reals)

theorem Real.add_of_LIM {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
  LIM a + LIM b = LIM (a + b) := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a + LIM b = LIM (a + b)
  have hab := Sequence.add_cauchy ha hba:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a + LIM b = LIM (a + b)
  simp_rw [LIM_def ha, LIM_def hb, LIM_def hab]a:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ⟦CauchySequence.mk' ha⟧ + ⟦CauchySequence.mk' hb⟧ = ⟦CauchySequence.mk' hab⟧
  convert Quotient.liftOn₂_mk _ _ _ _h.e'_3.h.e'_3a:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a + b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ CauchySequence.mk' hab =
  if h :
      { n₀ := 0,
          seq := fun n =>
            if n ≥ 0 then
              ((fun n => CauchySequence.toSequence.seq ↑n) + fun n => CauchySequence.toSequence.seq ↑n) n.toNat
            else 0,
          vanish := ⋯ }.isCauchy then
    CauchySequence.mk' h
  else 0
  rw [dif_pos _]All goals completed! 🐙

Proposition 5.3.10 (Product of Cauchy sequences is Cauchy)

theorem declaration uses 'sorry'Sequence.mul_cauchy {a b:ℕ → ℚ}  (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) : (a * b:Sequence).isCauchy := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (a * b) n.toNat else 0, vanish := ⋯ }.isCauchy
  sorryAll goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem declaration uses 'sorry'Sequence.mul_equiv_left {a a':ℕ → ℚ} (b:ℕ → ℚ) (haa': Sequence.equiv a a') :
  Sequence.equiv (a * b) (a' * b) := bya:ℕ → ℚa':ℕ → ℚb:ℕ → ℚhaa':equiv a a'⊢ equiv (a * b) (a' * b)
  sorryAll goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Sequence.mul_equiv_right {b b':ℕ → ℚ} (a:ℕ → ℚ) (hbb': Sequence.equiv b b') :
  Sequence.equiv (a * b) (a * b') := byb:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':equiv b b'⊢ equiv (a * b) (a * b')
  simp_rw [mul_comm]b:ℕ → ℚb':ℕ → ℚa:ℕ → ℚhbb':equiv b b'⊢ equiv (b * a) (b' * a)
  exact mul_equiv_left a hbb'All goals completed! 🐙

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Sequence.mul_equiv {a b a' b':ℕ → ℚ} (haa': Sequence.equiv a a') (hbb': Sequence.equiv b b') :
  Sequence.equiv (a * b) (a' * b') := equiv_trans (mul_equiv_left b haa') (mul_equiv_right a' hbb')

Definition 5.3.9 (Product of reals)

noncomputable instance Real.mul_inst : Mul Real where
  mul := fun x y ↦
    Quotient.liftOn₂ x y (fun a b ↦ LIM (a * b)) (byx:Realy:Real⊢ ∀ (a₁ b₁ a₂ b₂ : CauchySequence),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)) a₁ b₁ =
        (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)) a₂ b₂
      intro a b a' b' haa' hbb'x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)) a b =
  (fun a b => LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)) a' b'
      change LIM ((a:ℕ → ℚ) * (b:ℕ → ℚ)) = LIM ((a':ℕ → ℚ) * (b':ℕ → ℚ))x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n) =
  LIM ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)
      rw [LIM_eq_LIM]x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.equiv ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)
  ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0,
    seq := fun n =>
      if n ≥ 0 then ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n) n.toNat
      else 0,
    vanish := ⋯ }.isCauchyhbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0,
    seq := fun n =>
      if n ≥ 0 then ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n) n.toNat
      else 0,
    vanish := ⋯ }.isCauchy
      .x:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ Sequence.equiv ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n)
  ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n) exact Sequence.mul_equiv haa' hbb'All goals completed! 🐙
      all_goals apply Sequence.mul_cauchyhb.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then CauchySequence.toSequence.seq ↑n.toNat else 0, vanish := ⋯ }.isCauchyhb.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then CauchySequence.toSequence.seq ↑n.toNat else 0, vanish := ⋯ }.isCauchy
      all_goals rw [CauchySequence.coe_to_sequence]hb.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy
      .ha.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact a.cauchyAll goals completed! 🐙
      .ha.hbx:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact b.cauchyAll goals completed! 🐙
      .hb.hax:Realy:Reala:CauchySequenceb:CauchySequencea':CauchySequenceb':CauchySequencehaa':a ≈ a'hbb':b ≈ b'⊢ CauchySequence.toSequence.isCauchy exact a'.cauchyAll goals completed! 🐙
      exact b'.cauchyAll goals completed! 🐙
      )

theorem Real.mul_of_LIM {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
  LIM a * LIM b = LIM (a * b) := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a * LIM b = LIM (a * b)
  have hab := Sequence.mul_cauchy ha hba:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a * LIM b = LIM (a * b)
  simp_rw [LIM_def ha, LIM_def hb, LIM_def hab]a:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ⟦CauchySequence.mk' ha⟧ * ⟦CauchySequence.mk' hb⟧ = ⟦CauchySequence.mk' hab⟧
  convert Quotient.liftOn₂_mk _ _ _ _h.e'_3.h.e'_3a:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhab:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ CauchySequence.mk' hab =
  if h :
      { n₀ := 0,
          seq := fun n =>
            if n ≥ 0 then
              ((fun n => CauchySequence.toSequence.seq ↑n) * fun n => CauchySequence.toSequence.seq ↑n) n.toNat
            else 0,
          vanish := ⋯ }.isCauchy then
    CauchySequence.mk' h
  else 0
  rw [dif_pos _]All goals completed! 🐙

instance Real.instRatCast : RatCast Real where
  ratCast := fun q ↦
    Quotient.mk _ (CauchySequence.mk' (a := fun _ ↦ q) (Sequence.isCauchy_of_const q))

theorem Real.ratCast_def (q:ℚ) : (q:Real) = LIM (fun _ ↦ q) := byq:ℚ⊢ ↑q = LIM fun x => q
  rw [LIM_def]q:ℚ⊢ ↑q = ⟦CauchySequence.mk' ?m.320979⟧q:ℚ⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then q else 0, vanish := ⋯ }.isCauchy
  rflAll goals completed! 🐙

Exercise 5.3.3

@[simp]
theorem declaration uses 'sorry'Real.ratCast_inj (q r:ℚ) : (q:Real) = (r:Real) ↔ q = r := byq:ℚr:ℚ⊢ ↑q = ↑r ↔ q = r
  sorryAll goals completed! 🐙

instance Real.instOfNat {n:ℕ} : OfNat Real n where
  ofNat := ((n:ℚ):Real)

instance Real.instNatCast : NatCast Real where
  natCast n := ((n:ℚ):Real)

@[simp]
theorem Real.LIM_zero : LIM (fun _ ↦ (0:ℚ)) = 0 := by⊢ (LIM fun x => 0) = 0
  rw [←ratCast_def 0]⊢ ↑0 = 0
  rflAll goals completed! 🐙

instance Real.instIntCast : IntCast Real where
  intCast n := ((n:ℚ):Real)

theorem declaration uses 'sorry'Real.add_of_ratCast (a b:ℚ) : (a:Real) + (b:Real) = (a+b:ℚ) := bya:ℚb:ℚ⊢ ↑a + ↑b = ↑(a + b) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.mul_of_ratCast (a b:ℚ) : (a:Real) * (b:Real) = (a*b:ℚ) := bya:ℚb:ℚ⊢ ↑a * ↑b = ↑(a * b) sorryAll goals completed! 🐙

noncomputable instance Real.instNeg : Neg Real where
  neg := fun x ↦ ((-1:ℚ):Real) * x

theorem declaration uses 'sorry'Real.neg_of_ratCast (a:ℚ) : -(a:Real) = (-a:ℚ) := bya:ℚ⊢ -↑a = ↑(-a) sorryAll goals completed! 🐙

It may be possible to omit the Cauchy sequence hypothesis here.

theorem declaration uses 'sorry'Real.neg_of_LIM (a:ℕ → ℚ) (ha: (a:Sequence).isCauchy) : -LIM a = LIM (-a) := bya:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ -LIM a = LIM (-a) sorryAll goals completed! 🐙

Proposition 5.3.11

noncomputable instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.addGroup_inst : AddGroup Real :=
AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Real), a + b + c = a + (b + c) sorryAll goals completed! 🐙) (by⊢ ∀ (a : Real), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Real), -a + a = 0 sorryAll goals completed! 🐙)

theorem Real.sub_eq_add_neg (x y:Real) : x - y = x + (-y) := rfl

It may be possible to omit the Cauchy sequence hypothesis here.

theorem declaration uses 'sorry'Real.sub_of_LIM (a b:ℕ → ℚ) (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
  LIM a - LIM b = LIM (a - b) := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a - LIM b = LIM (a - b) sorryAll goals completed! 🐙

Proposition 5.3.12 (laws of algebra)

noncomputable instance declaration uses 'sorry'Real.instAddCommGroup : AddCommGroup Real where
  add_comm := by⊢ ∀ (a b : Real), a + b = b + a sorryAll goals completed! 🐙

Proposition 5.3.12 (laws of algebra)

noncomputable instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.instCommMonoid : CommMonoid Real where
  mul_comm := by⊢ ∀ (a b : Real), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Real), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Real), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Real), a * 1 = a sorryAll goals completed! 🐙

Proposition 5.3.12 (laws of algebra)

noncomputable instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.instCommRing : CommRing Real where
  left_distrib := by⊢ ∀ (a b c : Real), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Real), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Real), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Real), a * 0 = 0 sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Real), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  natCast_succ := by⊢ ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 sorryAll goals completed! 🐙
  intCast_negSucc := by⊢ ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) sorryAll goals completed! 🐙

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.ratCast_hom : ℚ →+* Real where
  toFun := RatCast.ratCast
  map_zero' := by⊢ RatCast.ratCast 0 = 0 sorryAll goals completed! 🐙
  map_one' := by⊢ RatCast.ratCast 1 = 1 sorryAll goals completed! 🐙
  map_add' := by⊢ ∀ (x y : ℚ), RatCast.ratCast (x + y) = RatCast.ratCast x + RatCast.ratCast y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : ℚ), RatCast.ratCast (x * y) = RatCast.ratCast x * RatCast.ratCast y sorryAll goals completed! 🐙

Definition 5.3.12 (sequences bounded away from zero). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

abbrev bounded_away_zero (a:ℕ → ℚ) : Prop :=
  ∃ (c:ℚ), c > 0 ∧ ∀ n, |a n| ≥ c

theorem bounded_away_zero_def (a:ℕ → ℚ) : bounded_away_zero a ↔
  ∃ (c:ℚ), c > 0 ∧ ∀ n, |a n| ≥ c := bya:ℕ → ℚ⊢ bounded_away_zero a ↔ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c rflAll goals completed! 🐙

Examples 5.3.13

declaration uses 'sorry'example : bounded_away_zero (fun n ↦ (-1)^n) := by⊢ bounded_away_zero fun n => (-1) ^ n sorryAll goals completed! 🐙

Examples 5.3.13

declaration uses 'sorry'example : ¬ bounded_away_zero (fun n ↦ 10^(-(n:ℤ)-1)) := by⊢ ¬bounded_away_zero fun n => 10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Examples 5.3.13

declaration uses 'sorry'example : ¬ bounded_away_zero (fun n ↦ 1 - 10^(-(n:ℤ))) := by⊢ ¬bounded_away_zero fun n => 1 - 10 ^ (-↑n) sorryAll goals completed! 🐙

Examples 5.3.13

declaration uses 'sorry'example : bounded_away_zero (fun n ↦ 10^(n+1)) := by⊢ bounded_away_zero fun n => 10 ^ (n + 1) sorryAll goals completed! 🐙

Examples 5.3.13

declaration uses 'sorry'example : ((fun (n:ℕ) ↦ (10:ℚ)^(n+1)):Sequence).isBounded := by⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 10 ^ (n + 1)) n.toNat else 0, vanish := ⋯ }.isBounded sorryAll goals completed! 🐙

Lemma 5.3.14

theorem declaration uses 'sorry'Real.bounded_away_zero_of_nonzero {x:Real} (hx: x ≠ 0) : ∃ a:ℕ → ℚ, (a:Sequence).isCauchy ∧ bounded_away_zero a ∧ x = LIM a := byx:Realhx:x ≠ 0⊢ ∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ bounded_away_zero a ∧ x = LIM a
  -- This proof is written to follow the structure of the original text.
  obtain ⟨ b, hb, rfl ⟩ := eq_lim xintro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhx:LIM b ≠ 0⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  simp only [←LIM_zero, ne_eq] at hxintro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhx:¬LIM b = LIM fun x => 0⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  rw [LIM_eq_LIM hb (by convert Sequence.isCauchy_of_const 0), Sequence.equiv_iff] at hxintro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhx:¬∀ ε > 0, ∃ N, ∀ n ≥ N, |b n - 0| ≤ ε⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  simp at hxintro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhx:∃ x, 0 < x ∧ ∀ (x_1 : ℕ), ∃ x_2, x_1 ≤ x_2 ∧ x < |b x_2|⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  obtain ⟨ ε, hε, hx ⟩ := hxintro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  have hb' := (Sequence.isCauchy_of_coe _).mp hb (ε/2) (half_pos hε)intro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|hb':∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  obtain ⟨ N, hb' ⟩ := hb'intro.intro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  obtain ⟨n₀, hn₀, hx ⟩ := hx Nintro.intro.intro.intro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  have how : ∀ j ≥ N, |b j| ≥ ε/2 := byx:Realhx:x ≠ 0⊢ ∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ bounded_away_zero a ∧ x = LIM a sorryAll goals completed! 🐙
  set a : ℕ → ℚ := fun n ↦ if n < n₀ then (ε/2) else b nintro.intro.intro.intro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b n⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  have not_hard : Sequence.equiv a b := byx:Realhx:x ≠ 0⊢ ∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ bounded_away_zero a ∧ x = LIM a sorryAll goals completed! 🐙
  have ha :(a:Sequence).isCauchy := (Sequence.equiv_of_cauchy not_hard).mpr hbintro.intro.intro.intro.intro.intro.introb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∃ a,
  { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧
    bounded_away_zero a ∧ LIM b = LIM a
  refine ⟨ a, ha, ?_, ?_ ⟩intro.intro.intro.intro.intro.intro.intro.refine_1b:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ bounded_away_zero aintro.intro.intro.intro.intro.intro.intro.refine_2b:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM b = LIM a
  .intro.intro.intro.intro.intro.intro.intro.refine_1b:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ bounded_away_zero a rw [bounded_away_zero_def]intro.intro.intro.intro.intro.intro.intro.refine_1b:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c
    use ε/2, half_pos hεrightb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∀ (n : ℕ), |a n| ≥ ε / 2
    intro nrightb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕ⊢ |a n| ≥ ε / 2
    by_cases hn: n < n₀posb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕhn:n < n₀⊢ |a n| ≥ ε / 2negb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕhn:¬n < n₀⊢ |a n| ≥ ε / 2
    all_goals simp [a, hn]negb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕhn:¬n < n₀⊢ ε / 2 ≤ |b n|
    .posb:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕhn:n < n₀⊢ ε / 2 ≤ |ε / 2| exact le_abs_self _All goals completed! 🐙
    apply howneg.ab:ℕ → ℚhb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyε:ℚhε:0 < εhx✝:∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ ε < |b x_1|N:ℕhb':∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (b j) (b k) ≤ ε / 2n₀:ℕhn₀:N ≤ n₀hx:ε < |b n₀|how:∀ j ≥ N, |b j| ≥ ε / 2a:ℕ → ℚ := fun n => if n < n₀ then ε / 2 else b nnot_hard:Sequence.equiv a bha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕhn:¬n < n₀⊢ n ≥ N
    linarithAll goals completed! 🐙
  rw[(LIM_eq_LIM ha hb).mpr not_hard]All goals completed! 🐙

This result was not explicitly stated in the text, but is needed in the theory. It's a good exercise, so I'm setting it as such.

theorem declaration uses 'sorry'Real.lim_of_bounded_away_zero {a:ℕ → ℚ} (ha: bounded_away_zero a) (ha_cauchy: (a:Sequence).isCauchy) :
  LIM a ≠ 0 := bya:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a ≠ 0
   sorryAll goals completed! 🐙

theorem Real.bounded_away_zero_nonzero {a:ℕ → ℚ} (ha: bounded_away_zero a) (n: ℕ) : a n ≠ 0 := bya:ℕ → ℚha:bounded_away_zero an:ℕ⊢ a n ≠ 0
   obtain ⟨ c, hc, ha ⟩ := haintro.introa:ℕ → ℚn:ℕc:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ c⊢ a n ≠ 0
   replace ha := ha nintro.introa:ℕ → ℚn:ℕc:ℚhc:c > 0ha:|a n| ≥ c⊢ a n ≠ 0; contrapose! haintro.introa:ℕ → ℚn:ℕc:ℚhc:c > 0ha:a n = 0⊢ |a n| < c; simp [ha, hc]All goals completed! 🐙

Lemma 5.3.15

theorem Real.inv_of_bounded_away_zero_cauchy {a:ℕ → ℚ} (ha: bounded_away_zero a) (ha_cauchy: (a:Sequence).isCauchy) :
  ((a⁻¹:ℕ → ℚ):Sequence).isCauchy := bya:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy
  -- This proof is written to follow the structure of the original text.
  have ha' (n:ℕ) : a n ≠ 0 := bounded_away_zero_nonzero ha na:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyha':∀ (n : ℕ), a n ≠ 0⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy
  rw [bounded_away_zero_def] at haa:ℕ → ℚha:∃ c > 0, ∀ (n : ℕ), |a n| ≥ cha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyha':∀ (n : ℕ), a n ≠ 0⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy
  obtain ⟨ c, hc, ha ⟩ := haintro.introa:ℕ → ℚha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ c⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy
  simp_rw [Sequence.isCauchy_of_coe, Section_4_3.dist_eq] at ha_cauchy ⊢intro.introa:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ ε⊢ ∀ ε > 0, ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a⁻¹ j - a⁻¹ k| ≤ ε
  intro ε hεintro.introa:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ εε:ℚhε:ε > 0⊢ ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a⁻¹ j - a⁻¹ k| ≤ ε
  replace ha_cauchy := ha_cauchy (c^2 * ε) (bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cha_cauchy:∀ ε > 0, ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ εε:ℚhε:ε > 0⊢ c ^ 2 * ε > 0 positivityAll goals completed! 🐙)
  obtain ⟨ N, ha_cauchy ⟩ := ha_cauchyintro.intro.introa:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy:∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ c ^ 2 * ε⊢ ∃ N, ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a⁻¹ j - a⁻¹ k| ≤ ε
  use Nha:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy:∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ c ^ 2 * ε⊢ ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a⁻¹ j - a⁻¹ k| ≤ ε
  intro n m ⟨hn, hm⟩ha:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕha_cauchy:∀ (j k : ℕ), j ≥ N ∧ k ≥ N → |a j - a k| ≤ c ^ 2 * εn:ℕm:ℕhn:n ≥ Nhm:m ≥ N⊢ |a⁻¹ n - a⁻¹ m| ≤ ε
  replace ha_cauchy := ha_cauchy n m ⟨hn, hm⟩ha:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a⁻¹ n - a⁻¹ m| ≤ ε
  calc
    _ = |(a m - a n) / (a m * a n)| := bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a⁻¹ n - a⁻¹ m| = |(a m - a n) / (a m * a n)|
      congre_aa:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ a⁻¹ n - a⁻¹ m = (a m - a n) / (a m * a n)
      field_simp [ha' m, ha' n]e_aa:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ a m * a n = a n * a m ∨ a m - a n = 0
      simp [mul_comm]All goals completed! 🐙
    _ ≤ |a m - a n| / c^2 := bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |(a m - a n) / (a m * a n)| ≤ |a m - a n| / c ^ 2
      rw [abs_div, abs_mul, sq]a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a m - a n| / (|a m| * |a n|) ≤ |a m - a n| / (c * c)
      gcongrh.h₁a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a m|h.h₂a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a n|
      .h.h₁a:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ≤ |a m| exact ha mAll goals completed! 🐙
      exact ha nAll goals completed! 🐙
    _ = |a n - a m| / c^2 := bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a m - a n| / c ^ 2 = |a n - a m| / c ^ 2
      rw [abs_sub_comm]All goals completed! 🐙
    _ ≤ (c^2 * ε) / c^2 := bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ |a n - a m| / c ^ 2 ≤ c ^ 2 * ε / c ^ 2
      gcongrAll goals completed! 🐙
    _ = ε := bya:ℕ → ℚha':∀ (n : ℕ), a n ≠ 0c:ℚhc:c > 0ha:∀ (n : ℕ), |a n| ≥ cε:ℚhε:ε > 0N:ℕn:ℕm:ℕhn:n ≥ Nhm:m ≥ Nha_cauchy:|a n - a m| ≤ c ^ 2 * ε⊢ c ^ 2 * ε / c ^ 2 = ε
      field_simp [hc]All goals completed! 🐙

Lemma 5.3.17 (Reciprocation is well-defined)

theorem Real.inv_of_equiv {a b:ℕ → ℚ} (ha: bounded_away_zero a) (ha_cauchy: (a:Sequence).isCauchy) (hb: bounded_away_zero b) (hb_cauchy: (b:Sequence).isCauchy) (hlim: LIM a = LIM b) :
  LIM a⁻¹ = LIM b⁻¹ := bya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹
  -- This proof is written to follow the structure of the original text.
  set P := LIM a⁻¹ * LIM a * LIM b⁻¹a:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹⊢ LIM a⁻¹ = LIM b⁻¹
  have ha' (n:ℕ) : a n ≠ 0 := bounded_away_zero_nonzero ha na:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0⊢ LIM a⁻¹ = LIM b⁻¹
  have hb' (n:ℕ) : b n ≠ 0 := bounded_away_zero_nonzero hb na:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0⊢ LIM a⁻¹ = LIM b⁻¹
  have hainv_cauchy := Real.inv_of_bounded_away_zero_cauchy ha ha_cauchya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a⁻¹ = LIM b⁻¹
  have hbinv_cauchy := Real.inv_of_bounded_away_zero_cauchy hb hb_cauchya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a⁻¹ = LIM b⁻¹
  have haainv_cauchy := Sequence.mul_cauchy hainv_cauchy ha_cauchya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a⁻¹ = LIM b⁻¹
  have habinv_cauchy := Sequence.mul_cauchy hainv_cauchy hb_cauchya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a⁻¹ = LIM b⁻¹
  have claim1 : P = LIM b⁻¹ := bya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹
    unfold Pa:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM a⁻¹ * LIM a * LIM b⁻¹ = LIM b⁻¹
    rw [mul_of_LIM hainv_cauchy ha_cauchy, mul_of_LIM haainv_cauchy hbinv_cauchy]a:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchy⊢ LIM (a⁻¹ * a * b⁻¹) = LIM b⁻¹
    rcongr ne_a.ha:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchyn:ℕ⊢ (a⁻¹ * a * b⁻¹) n = b⁻¹ n
    simp [ha' n]All goals completed! 🐙
  have claim2 : P = LIM a⁻¹ := bya:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM b⊢ LIM a⁻¹ = LIM b⁻¹
    unfold Pa:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchyclaim1:P = LIM b⁻¹⊢ LIM a⁻¹ * LIM a * LIM b⁻¹ = LIM a⁻¹
    rw [hlim, mul_of_LIM hainv_cauchy hb_cauchy, mul_of_LIM habinv_cauchy hbinv_cauchy]a:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchyclaim1:P = LIM b⁻¹⊢ LIM (a⁻¹ * b * b⁻¹) = LIM a⁻¹
    rcongr ne_a.ha:ℕ → ℚb:ℕ → ℚha:bounded_away_zero aha_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyhb:bounded_away_zero bhb_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhlim:LIM a = LIM bP:Real := LIM a⁻¹ * LIM a * LIM b⁻¹ha':∀ (n : ℕ), a n ≠ 0hb':∀ (n : ℕ), b n ≠ 0hainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then a⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhbinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then b⁻¹ n.toNat else 0, vanish := ⋯ }.isCauchyhaainv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * a) n.toNat else 0, vanish := ⋯ }.isCauchyhabinv_cauchy:{ n₀ := 0, seq := fun n => if n ≥ 0 then (a⁻¹ * b) n.toNat else 0, vanish := ⋯ }.isCauchyclaim1:P = LIM b⁻¹n:ℕ⊢ (a⁻¹ * b * b⁻¹) n = a⁻¹ n
    simp [hb' n]All goals completed! 🐙
  simp [←claim1, ←claim2]All goals completed! 🐙

open Classical in
/-- Definition 5.3.16 (Reciprocation of real numbers).  Requires classical logic because we need to assign a "junk" value to the inverse of 0.  -/
noncomputable instance Real.instInv : Inv Real where
  inv x := if h: x ≠ 0 then LIM (bounded_away_zero_of_nonzero h).choose⁻¹ else 0

theorem Real.inv_def {a:ℕ → ℚ} (h: bounded_away_zero a) (hc: (a:Sequence).isCauchy) : (LIM a)⁻¹ = LIM a⁻¹ := bya:ℕ → ℚh:bounded_away_zero ahc:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ (LIM a)⁻¹ = LIM a⁻¹
  set x := LIM aa:ℕ → ℚh:bounded_away_zero ahc:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyx:Real := LIM a⊢ x⁻¹ = LIM a⁻¹
  have hx : x ≠ 0 := lim_of_bounded_away_zero h hca:ℕ → ℚh:bounded_away_zero ahc:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyx:Real := LIM ahx:x ≠ 0⊢ x⁻¹ = LIM a⁻¹
  set hb := bounded_away_zero_of_nonzero hxa:ℕ → ℚh:bounded_away_zero ahc:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyx:Real := LIM ahx:x ≠ 0hb:∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ bounded_away_zero a ∧ x = LIM a := bounded_away_zero_of_nonzero hx⊢ x⁻¹ = LIM a⁻¹
  simp only [instInv, ne_eq, Classical.dite_not, hx, ↓reduceDIte, Pi.inv_apply]a:ℕ → ℚh:bounded_away_zero ahc:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyx:Real := LIM ahx:x ≠ 0hb:∃ a, { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ bounded_away_zero a ∧ x = LIM a := bounded_away_zero_of_nonzero hx⊢ LIM ⋯.choose⁻¹ = LIM a⁻¹
  apply inv_of_equiv hb.choose_spec.2.1 hb.choose_spec.1 h hc hb.choose_spec.2.2.symmAll goals completed! 🐙

@[simp]
theorem Real.inv_zero : (0:Real)⁻¹ = 0 := by⊢ 0⁻¹ = 0
  simp [Inv.inv]All goals completed! 🐙

theorem declaration uses 'sorry'Real.self_mul_inv {x:Real} (hx: x ≠ 0) : x * x⁻¹ = 1 := byx:Realhx:x ≠ 0⊢ x * x⁻¹ = 1
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.inv_mul_self {x:Real} (hx: x ≠ 0) : x * x⁻¹ = 1 := byx:Realhx:x ≠ 0⊢ x * x⁻¹ = 1
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.inv_of_ratCast (q:ℚ) : (q:Real)⁻¹ = (q⁻¹:ℚ) := byq:ℚ⊢ (↑q)⁻¹ = ↑q⁻¹
  sorryAll goals completed! 🐙

Default definition of division

noncomputable instance Real.instDivInvMonoid : DivInvMonoid Real wheretheorem Real.div_eq (x y:Real) : x/y = x * y⁻¹ := byx:Realy:Real⊢ x / y = x * y⁻¹ rflAll goals completed! 🐙

noncomputable instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.instField : Field Real where
  exists_pair_ne := by⊢ ∃ x y, x ≠ y sorryAll goals completed! 🐙
  mul_inv_cancel := by⊢ ∀ (a : Real), a ≠ 0 → a * a⁻¹ = 1 sorryAll goals completed! 🐙
  inv_zero := by⊢ 0⁻¹ = 0 sorryAll goals completed! 🐙
  ratCast_def := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den sorryAll goals completed! 🐙
  qsmul := _
  nnqsmul := _

theorem declaration uses 'sorry'Real.mul_right_cancel₀ {x y z:Real} (hz: z ≠ 0) (h: x * z = y * z) : x = y := byx:Realy:Realz:Realhz:z ≠ 0h:x * z = y * z⊢ x = y sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.mul_right_nocancel : ¬ ∀ (x y z:Real), (hz: z = 0) → (x * z = y * z) → x = y := by⊢ ¬∀ (x y z : Real), z = 0 → x * z = y * z → x = y sorryAll goals completed! 🐙

Exercise 5.3.4

theorem declaration uses 'sorry'Real.equiv_of_bounded {a b:ℕ → ℚ} (ha: (a:Sequence).isBounded) (hab: Sequence.equiv a b) : (b:Sequence).isBounded := bya:ℕ → ℚb:ℕ → ℚha:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBoundedhab:Sequence.equiv a b⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isBounded sorryAll goals completed! 🐙

Exercise 5.3.5

theorem declaration uses 'sorry'Real.LIM_of_harmonic : LIM (fun n ↦ 1/n) = 0 := by⊢ (LIM fun n => 1 / ↑n) = 0 sorryAll goals completed! 🐙

end Chapter5