finish Lemma 5.3.15

Author: teorth

Analysis/Section_4_3.lean

@@ -42,7 +42,7 @@ theorem abs_eq_abs (x: ℚ) : abs x = |x| := by
 abbrev dist (x y : ℚ) := |x - y|
 
 /-- Definition 4.2 (Distance).  We avoid the Mathlib notion of distance here because it is real-valued.  -/
-theorem dist_eq (x y: ℚ) : dist x y = |x-y| := by simp [Rat.dist_eq]
+theorem dist_eq (x y: ℚ) : dist x y = |x-y| := rfl
 
 /-- Proposition 4.3.3(a) / Exercise 4.3.1 -/
 theorem abs_nonneg (x: ℚ) : |x| ≥ 0 := by sorry

Analysis/Section_5_3.lean

@@ -363,7 +363,32 @@ theorem Real.lim_of_bounded_away_zero {a:ℕ → ℚ} (ha: bounded_away_zero a)
 theorem Real.inv_of_bounded_away_zero_cauchy {a:ℕ → ℚ} (ha: bounded_away_zero a) (ha_cauchy: (a:Sequence).isCauchy) :
   ((a⁻¹:ℕ → ℚ):Sequence).isCauchy := by
   -- This proof is written to follow the structure of the original text.
-  sorry -- TODO
+  rw [bounded_away_zero_def] at ha
+  obtain ⟨ c, hc, ha ⟩ := ha
+  have ha' (n:ℕ) : a n ≠ 0 := by replace ha := ha n; contrapose! ha; simp [ha, hc]
+  simp_rw [Sequence.isCauchy_of_coe, Section_4_3.dist_eq] at ha_cauchy ⊢
+  intro ε hε
+  replace ha_cauchy := ha_cauchy (c^2 * ε) (by positivity)
+  obtain ⟨ N, ha_cauchy ⟩ := ha_cauchy
+  use N
+  intro n m ⟨hn, hm⟩
+  replace ha_cauchy := ha_cauchy n m ⟨hn, hm⟩
+  calc
+    _ = |(a m - a n) / (a m * a n)| := by
+      congr
+      field_simp [ha' m, ha' n]
+      simp [mul_comm]
+    _ ≤ |a m - a n| / c^2 := by
+      rw [abs_div, abs_mul, sq]
+      gcongr
+      . exact ha m
+      exact ha n
+    _ = |a n - a m| / c^2 := by
+      rw [abs_sub_comm]
+    _ ≤ (c^2 * ε) / c^2 := by
+      gcongr
+    _ = ε := by
+      field_simp [hc]
 
 /-- 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) :