refactor(cau_seq): unify real.lim, complex.lim and cau_seq.lim (#433)

analysis/real.lean

@@ -278,10 +278,10 @@ instance : complete_space ℝ :=
     have : F j ⊆ F n :=
       bInter_subset_bInter_left (λ i h, @le_trans _ _ i n j h jn),
     exact lt_trans (hF_dist n _ _ (this (hG j)) (hG n)) (hn _ $ le_refl _) },
-  refine ⟨real.lim c, λ s h, _⟩,
+  refine ⟨cau_seq.lim c, λ s h, _⟩,
   rcases mem_nhds_iff_metric.1 h with ⟨ε, ε0, hε⟩,
   cases exists_forall_ge_and (hg _ $ half_pos ε0)
-    (real.equiv_lim c _ $ half_pos ε0) with n hn,
+    (cau_seq.equiv_lim c _ $ half_pos ε0) with n hn,
   cases hn _ (le_refl _) with h₁ h₂,
   refine sets_of_superset _ (hF n) (subset.trans _ $
     subset.trans (ball_half_subset (G n) h₂) hε),

data/complex/basic.lean

@@ -378,9 +378,6 @@ by rw [← of_real_nat_cast, abs_of_nonneg (nat.cast_nonneg n)]
 lemma norm_sq_eq_abs (x : ℂ) : norm_sq x = abs x ^ 2 :=
 by rw [abs, pow_two, real.mul_self_sqrt (norm_sq_nonneg _)]
 
-noncomputable def lim (f : ℕ → ℂ) : ℂ :=
-⟨real.lim (λ n, (f n).re), real.lim (λ n, (f n).im)⟩
-
 theorem is_cau_seq_re (f : cau_seq ℂ abs) : is_cau_seq abs' (λ n, (f n).re) :=
 λ ε ε0, (f.cauchy ε0).imp $ λ i H j ij,
 lt_of_le_of_lt (by simpa using abs_re_le_abs (f j - f i)) (H _ ij)
@@ -389,112 +386,65 @@ theorem is_cau_seq_im (f : cau_seq ℂ abs) : is_cau_seq abs' (λ n, (f n).im) :
 λ ε ε0, (f.cauchy ε0).imp $ λ i H j ij,
 lt_of_le_of_lt (by simpa using abs_im_le_abs (f j - f i)) (H _ ij)
 
+noncomputable def cau_seq_re (f : cau_seq ℂ abs) : cau_seq ℝ abs' :=
+⟨_, is_cau_seq_re f⟩
+
+noncomputable def cau_seq_im (f : cau_seq ℂ abs) : cau_seq ℝ abs' :=
+⟨_, is_cau_seq_im f⟩
+
 lemma is_cau_seq_abs {f : ℕ → ℂ} (hf : is_cau_seq abs f) :
   is_cau_seq abs' (abs ∘ f) :=
 λ ε ε0, let ⟨i, hi⟩ := hf ε ε0 in
 ⟨i, λ j hj, lt_of_le_of_lt (abs_abs_sub_le_abs_sub _ _) (hi j hj)⟩
 
-theorem equiv_lim (f : cau_seq ℂ abs) : f ≈ cau_seq.const abs (lim f) :=
+noncomputable def lim_aux (f : cau_seq ℂ abs) : ℂ :=
+⟨cau_seq.lim (cau_seq_re f), cau_seq.lim (cau_seq_im f)⟩
+
+theorem equiv_lim_aux (f : cau_seq ℂ abs) : f ≈ cau_seq.const abs (lim_aux f) :=
 λ ε ε0, (exists_forall_ge_and
-  (real.equiv_lim ⟨_, is_cau_seq_re f⟩ _ (half_pos ε0))
-  (real.equiv_lim ⟨_, is_cau_seq_im f⟩ _ (half_pos ε0))).imp $
+  (cau_seq.equiv_lim ⟨_, is_cau_seq_re f⟩ _ (half_pos ε0))
+  (cau_seq.equiv_lim ⟨_, is_cau_seq_im f⟩ _ (half_pos ε0))).imp $
 λ i H j ij, begin
   cases H _ ij with H₁ H₂,
   apply lt_of_le_of_lt (abs_le_abs_re_add_abs_im _),
-  simpa using add_lt_add H₁ H₂
+  dsimp [lim_aux] at *,
+  have := add_lt_add H₁ H₂,
+  rwa add_halves at this,
 end
 
+noncomputable instance : cau_seq.is_complete ℂ abs :=
+⟨λ f, ⟨lim_aux f, equiv_lim_aux f⟩⟩
+
 open cau_seq
 
-lemma re_const_equiv_of_const_equiv {f : cau_seq ℂ abs} (z : ℂ)
-  (h : const abs z ≈ f) :
-  const _root_.abs z.re ≈ ⟨(λ (n : ℕ), (f n).re), is_cau_seq_re f⟩  :=
-λ ε ε0, let ⟨i, hi⟩ := h ε ε0 in
-⟨i, λ j hji, show abs' (z.re - (f j).re) < ε,
-  by rw ← sub_re; exact lt_of_le_of_lt (abs_re_le_abs _) (hi j hji)⟩
-
-lemma im_const_equiv_of_const_equiv {f : cau_seq ℂ abs} (z : ℂ)
-  (h : const abs z ≈ f) :
-  const _root_.abs z.im ≈ ⟨(λ (n : ℕ), (f n).im), is_cau_seq_im f⟩  :=
-λ ε ε0, let ⟨i, hi⟩ := h ε ε0 in
-⟨i, λ j hji, show abs' (z.im - (f j).im) < ε,
-  by rw ← sub_im; exact lt_of_le_of_lt (abs_im_le_abs _) (hi j hji)⟩
-
-lemma eq_lim_of_const_equiv {f : cau_seq ℂ abs} {z : ℂ}
-  (h : const abs z ≈ f) : z = lim f :=
-complex.ext
-  (show z.re = real.lim (⟨complex.re ∘ f, is_cau_seq_re f⟩ : cau_seq ℝ abs'),
-    from real.eq_lim_of_const_equiv (re_const_equiv_of_const_equiv _ h))
-  (show z.im = real.lim (⟨complex.im ∘ f, is_cau_seq_im f⟩ : cau_seq ℝ abs'),
-    from real.eq_lim_of_const_equiv (im_const_equiv_of_const_equiv _ h))
-
-lemma lim_eq_of_equiv_const {f : cau_seq ℂ abs} {x : ℂ} (h : f ≈ const abs x) : lim f = x :=
-(eq_lim_of_const_equiv $ setoid.symm h).symm
-
-lemma lim_eq_lim_of_equiv {f g : cau_seq ℂ abs} (h : f ≈ g) : lim f = lim g :=
-lim_eq_of_equiv_const $ setoid.trans h $ equiv_lim g
-
-@[simp] lemma lim_const (x : ℂ) : lim (const abs x) = x :=
-lim_eq_of_equiv_const $ setoid.refl _
-
-lemma lim_add (f g : cau_seq ℂ abs) : lim f + lim g = lim ⇑(f + g) :=
-eq_lim_of_const_equiv $ show lim_zero (const abs (lim ⇑f + lim ⇑g) - (f + g)),
-  by rw [const_add, add_sub_comm];
-  exact add_lim_zero (setoid.symm (equiv_lim f)) (setoid.symm (equiv_lim g))
-
-lemma lim_mul_lim (f g : cau_seq ℂ abs) : lim f * lim g = lim ⇑(f * g) :=
-eq_lim_of_const_equiv $ show lim_zero (const abs (lim ⇑f * lim ⇑g) - f * g),
-  from have h : const abs (lim ⇑f * lim ⇑g) - f * g = g * (const abs (lim f) - f)
-      + const abs (lim f) * (const abs (lim g) - g) :=
-    by simp [mul_sub, mul_comm, const_mul, mul_add],
-  by rw h; exact add_lim_zero (mul_lim_zero _ (setoid.symm (equiv_lim f)))
-      (mul_lim_zero _ (setoid.symm (equiv_lim g)))
-
-lemma lim_mul (f : cau_seq ℂ abs) (x : ℂ) : lim f * x = lim ⇑(f * const abs x) :=
-by rw [← lim_mul_lim, lim_const]
-
-lemma lim_neg (f : cau_seq ℂ abs) : lim ⇑(-f) = -lim f :=
-lim_eq_of_equiv_const (show lim_zero (-f - const abs (-lim ⇑f)),
-  by rw [const_neg, sub_neg_eq_add, add_comm];
-  exact setoid.symm (equiv_lim f))
-
-lemma is_cau_seq_conj {f : ℕ → ℂ} (hf : is_cau_seq abs f) :
-  is_cau_seq abs (conj ∘ f) :=
-λ ε ε0, let ⟨i, hi⟩ := hf ε ε0 in
-⟨i, λ j hj, by rw [function.comp_apply, function.comp_apply, ← conj_sub, abs_conj];
-  exact hi j hj⟩
-
-lemma lim_conj (f : cau_seq ℂ abs) : lim (⟨conj ∘ f, is_cau_seq_conj f.2⟩ : cau_seq ℂ abs) = conj (lim f) :=
-complex.ext rfl (real.lim_neg ⟨_, is_cau_seq_im f⟩ : _)
-
-lemma lim_eq_zero_iff (f : cau_seq ℂ abs) : lim f = 0 ↔ lim_zero f :=
-⟨assume h,
-  by have hf := equiv_lim f;
-  rw h at hf;
-  exact (lim_zero_congr hf).mpr (const_lim_zero.mpr rfl),
-assume h,
-  have h₁ : f = (f - const abs (0 : ℂ)) := cau_seq.ext (λ n, by simp [sub_apply, const_apply]),
-  by rw h₁ at h; exact lim_eq_of_equiv_const h ⟩
-
-lemma lim_inv {f : cau_seq ℂ abs} (hf : ¬ lim_zero f) : lim ⇑(inv f hf) = (lim f)⁻¹ :=
-have hl : lim f ≠ 0 := by rwa ← lim_eq_zero_iff at hf,
-lim_eq_of_equiv_const $ show lim_zero (inv f hf - const abs (lim ⇑f)⁻¹),
-  from have h₁ : ∀ (g f : cau_seq ℂ abs) (hf : ¬ lim_zero f), lim_zero (g - f * inv f hf * g) :=
-    λ g f hf, by rw [← one_mul g, ← mul_assoc, ← sub_mul, mul_one, mul_comm, mul_comm f];
-    exact mul_lim_zero _ (setoid.symm (cau_seq.inv_mul_cancel _)),
-  have h₂ : lim_zero ((inv f hf - const abs (lim ⇑f)⁻¹) - (const abs (lim f) - f) *
-      (inv f hf * const abs (lim ⇑f)⁻¹)) :=
-    by rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add];
-    exact show lim_zero (inv f hf - const abs (lim ⇑f) * (inv f hf * const abs (lim ⇑f)⁻¹)
-      - (const abs (lim ⇑f)⁻¹ - f * (inv f hf * const abs (lim ⇑f)⁻¹))),
-    from sub_lim_zero
-      (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _)
-      (by rw [← mul_assoc]; exact h₁ _ _ _),
-  (lim_zero_congr h₂).mpr $ by rw mul_comm; exact mul_lim_zero _ (setoid.symm (equiv_lim f))
-
-lemma lim_abs (f : cau_seq ℂ abs) :
-  real.lim (⟨_, is_cau_seq_abs f.2⟩ : cau_seq ℝ abs') = abs (complex.lim f) :=
-real.lim_eq_of_equiv_const (λ ε ε0,
+lemma lim_eq_lim_im_add_lim_re (f : cau_seq ℂ abs) : lim f =
+  ↑(lim (cau_seq_re f)) + ↑(lim (cau_seq_im f)) * I :=
+lim_eq_of_equiv_const $
+calc f ≈ _ : equiv_lim_aux f
+... = cau_seq.const abs (↑(lim (cau_seq_re f)) + ↑(lim (cau_seq_im f)) * I) :
+  cau_seq.ext (λ _, complex.ext (by simp [lim_aux, cau_seq_re]) (by simp [lim_aux, cau_seq_im]))
+
+lemma lim_re (f : cau_seq ℂ abs) : lim (cau_seq_re f) = (lim f).re :=
+by rw [lim_eq_lim_im_add_lim_re]; simp
+
+lemma lim_im (f : cau_seq ℂ abs) : lim (cau_seq_im f) = (lim f).im :=
+by rw [lim_eq_lim_im_add_lim_re]; simp
+
+lemma is_cau_seq_conj (f : cau_seq ℂ abs) : is_cau_seq abs (λ n, conj (f n)) :=
+λ ε ε0, let ⟨i, hi⟩ := f.2 ε ε0 in
+⟨i, λ j hj, by rw [← conj_sub, abs_conj]; exact hi j hj⟩
+
+noncomputable def cau_seq_conj (f : cau_seq ℂ abs) : cau_seq ℂ abs := ⟨_, is_cau_seq_conj f⟩
+
+lemma lim_conj (f : cau_seq ℂ abs) : lim (cau_seq_conj f) = conj (lim f) :=
+complex.ext (by simp [cau_seq_conj, (lim_re _).symm, cau_seq_re])
+  (by simp [cau_seq_conj, (lim_im _).symm, cau_seq_im, (lim_neg _).symm]; refl)
+
+noncomputable def cau_seq_abs (f : cau_seq ℂ abs) : cau_seq ℝ abs' :=
+⟨_, is_cau_seq_abs f.2⟩
+
+lemma lim_abs (f : cau_seq ℂ abs) : lim (cau_seq_abs f) = abs (lim f) :=
+lim_eq_of_equiv_const (λ ε ε0,
 let ⟨i, hi⟩ := equiv_lim f ε ε0 in
 ⟨i, λ j hj, lt_of_le_of_lt (abs_abs_sub_le_abs_sub _ _) (hi j hj)⟩)
 

data/complex/exponential.lean

@@ -304,6 +304,8 @@ end
 
 open finset
 
+open cau_seq
+
 namespace complex
 
 lemma is_cau_abs_exp (z : ℂ) : is_cau_seq _root_.abs
@@ -394,8 +396,8 @@ have hj : ∀ j : ℕ, (range j).sum
     finset.sum_congr rfl (λ m hm, begin
       rw [add_pow, div_eq_mul_inv, sum_mul],
       refine finset.sum_congr rfl (λ i hi, _),
-      have h₁ : (choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2 (λ h,
-        by simpa [h, lt_irrefl] using choose_pos (nat.le_of_lt_succ (mem_range.1 hi))),
+      have h₁ : (choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2
+        (nat.pos_iff_ne_zero.1 (choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
       have h₂ := choose_mul_fact_mul_fact (nat.le_of_lt_succ $ finset.mem_range.1 hi),
       rw [← h₂, nat.cast_mul, nat.cast_mul, mul_inv', mul_inv'],
       simp only [mul_left_comm (choose m i : ℂ), mul_assoc, mul_left_comm (choose m i : ℂ)⁻¹,
@@ -422,9 +424,8 @@ by simp [exp_add, exp_neg, div_eq_mul_inv]
 begin
   dsimp [exp],
   rw [← lim_conj],
-  refine congr_arg lim _,
-  dsimp [exp', function.comp],
-  funext,
+  refine congr_arg lim (cau_seq.ext (λ _, _)),
+  dsimp [exp', function.comp, cau_seq_conj],
   rw ← sum_hom conj conj_zero conj_add,
   refine sum_congr rfl (λ n hn, _),
   rw [conj_div, conj_pow, ← of_real_nat_cast, conj_of_real]
@@ -795,18 +796,19 @@ open is_absolute_value
 
 /- TODO make this private and prove ∀ x -/
 lemma add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x :=
-show x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩ : cau_seq ℝ abs'),
-from real.le_lim (cau_seq.le_of_exists ⟨2,
-  λ j hj, show x + (1 : ℝ) ≤ ((range j).sum (λ m, (x ^ m / m.fact : ℂ))).re,
-    from have h₁ : (((λ m : ℕ, (x ^ m / m.fact : ℂ)) ∘ nat.succ) 0).re = x, by simp,
-    have h₂ : ((x : ℂ) ^ 0 / nat.fact 0).re = 1, by simp,
-    begin
-      rw [← nat.sub_add_cancel hj, sum_range_succ', sum_range_succ',
-        add_re, add_re, h₁, h₂, add_assoc, ← sum_hom complex.re zero_re add_re],
-      refine le_add_of_nonneg_of_le (zero_le_sum (λ m hm, _)) (le_refl _), dsimp [-nat.fact_succ],
-      rw [← of_real_pow, ← of_real_nat_cast, ← of_real_div, of_real_re],
-      exact div_nonneg (pow_nonneg hx _) (nat.cast_pos.2 (nat.fact_pos _)),
-    end⟩)
+calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩ : cau_seq ℝ abs') :
+  le_lim (cau_seq.le_of_exists ⟨2,
+    λ j hj, show x + (1 : ℝ) ≤ ((range j).sum (λ m, (x ^ m / m.fact : ℂ))).re,
+      from have h₁ : (((λ m : ℕ, (x ^ m / m.fact : ℂ)) ∘ nat.succ) 0).re = x, by simp,
+      have h₂ : ((x : ℂ) ^ 0 / nat.fact 0).re = 1, by simp,
+      begin
+        rw [← nat.sub_add_cancel hj, sum_range_succ', sum_range_succ',
+          add_re, add_re, h₁, h₂, add_assoc, ← sum_hom complex.re zero_re add_re],
+        refine le_add_of_nonneg_of_le (zero_le_sum (λ m hm, _)) (le_refl _), dsimp [-nat.fact_succ],
+        rw [← of_real_pow, ← of_real_nat_cast, ← of_real_div, of_real_re],
+        exact div_nonneg (pow_nonneg hx _) (nat.cast_pos.2 (nat.fact_pos _)),
+      end⟩)
+... = exp x : by rw [exp, complex.exp, ← cau_seq_re, lim_re]
 
 lemma one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x :=
 by linarith using [add_one_le_exp_of_nonneg hx]
@@ -883,7 +885,7 @@ lemma exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
   abs (exp x - (range n).sum (λ m, x ^ m / m.fact)) ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹) :=
 begin
   rw [← lim_const ((range n).sum _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs],
-  refine real.lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),
+  refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),
   show abs ((range j).sum (λ m, x ^ m / m.fact) - (range n).sum (λ m, x ^ m / m.fact))
     ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹),
   rw sum_range_sub_sum_range hj,

data/padics/hensel.lean

@@ -325,7 +325,7 @@ private def soln : ℤ_[p] := newton_cau_seq.lim
 
 private lemma soln_spec {ε : ℝ} (hε : ε > 0) :
   ∃ (N : ℕ), ∀ {i : ℕ}, i ≥ N → ∥soln - newton_cau_seq i∥ < ε :=
-cau_seq.lim_spec newton_cau_seq _ hε
+setoid.symm (cau_seq.equiv_lim newton_cau_seq) _ hε
 
 private lemma soln_deriv_norm : ∥F.derivative.eval soln∥ = ∥F.derivative.eval a∥ :=
 norm_deriv_eq newton_seq_deriv_norm

data/padics/padic_integers.lean

@@ -236,7 +236,7 @@ instance complete : cau_seq.is_complete ℤ_[p] norm :=
   have hqn : ∥cau_seq.lim (cau_seq_to_rat_cau_seq f)∥ ≤ 1,
     from padic_norm_e_lim_le zero_lt_one (λ _, padic_norm_z.le_one _),
   ⟨ ⟨_, hqn⟩,
-    by simpa [norm, padic_norm_z] using cau_seq.lim_spec (cau_seq_to_rat_cau_seq f) ⟩⟩
+    λ ε, by simpa [norm, padic_norm_z] using cau_seq.equiv_lim (cau_seq_to_rat_cau_seq f) ε⟩⟩
 
 end padic_int
 

data/padics/padic_numbers.lean

@@ -744,14 +744,14 @@ instance complete : cau_seq.is_complete ℚ_[p] norm :=
     ⟨λ n, f n, λ ε hε,
       let ⟨N, hN⟩ := is_cau f ↑ε (rat.cast_pos.2 hε) in ⟨N, λ j hj, rat.cast_lt.1 (hN _ hj)⟩⟩ in
   let ⟨q, hq⟩ := padic.complete' f' in
-  ⟨ q, λ ε hε,
+  ⟨ q, setoid.symm $ λ ε hε,
     let ⟨ε', hε'l, hε'r⟩ := exists_rat_btwn hε,
         ⟨N, hN⟩ := hq _ (by simpa using hε'l) in
     ⟨N, λ i hi, lt.trans (rat.cast_lt.2 (hN _ hi)) hε'r ⟩⟩⟩
 
 lemma padic_norm_e_lim_le {f : cau_seq ℚ_[p] norm} {a : ℝ} (ha : a > 0)
       (hf : ∀ i, ∥f i∥ ≤ a) : ∥f.lim∥ ≤ a :=
-let ⟨N, hN⟩ := cau_seq.lim_spec f _ ha in
+let ⟨N, hN⟩ := setoid.symm (cau_seq.equiv_lim f) _ ha in
 calc ∥f.lim∥ = ∥f.lim - f N + f N∥ : by simp
                 ... ≤ max (∥f.lim - f N∥) (∥f N∥) : padic_norm_e.nonarchimedean _ _
                 ... ≤ a : max_le (le_of_lt (hN _ (le_refl _))) (hf _)

data/real/basic.lean

@@ -386,99 +386,7 @@ begin
     exact ih _ ij }
 end
 
-noncomputable instance : cau_seq.is_complete ℝ abs :=
-⟨ λ f, let ⟨x, hx⟩ := cau_seq_converges f in
-  have lim_zero (const abs x - f), from lim_zero_sub_rev hx,
-  ⟨x, this⟩ ⟩
-
-section lim
-
-open cau_seq
-
-noncomputable def lim (f : ℕ → ℝ) : ℝ :=
-if hf : is_cau_seq abs f then
-  classical.some (cau_seq_converges ⟨f, hf⟩)
-else 0
-
-theorem equiv_lim (f : cau_seq ℝ abs) : f ≈ const abs (lim f) :=
-by simp [lim, f.is_cau]; cases f with f hf;
-   exact classical.some_spec (cau_seq_converges ⟨f, hf⟩)
-
-lemma eq_lim_of_const_equiv {f : cau_seq ℝ abs} {x : ℝ} (h : cau_seq.const abs x ≈ f) : x = lim f :=
-const_equiv.mp $ setoid.trans h $ equiv_lim f
-
-lemma lim_eq_of_equiv_const {f : cau_seq ℝ abs} {x : ℝ} (h : f ≈ cau_seq.const abs x) : lim f = x :=
-(eq_lim_of_const_equiv $ setoid.symm h).symm
-
-lemma lim_eq_lim_of_equiv {f g : cau_seq ℝ abs} (h : f ≈ g) : lim f = lim g :=
-lim_eq_of_equiv_const $ setoid.trans h $ equiv_lim g
-
-@[simp] lemma lim_const (x : ℝ) : lim (const abs x) = x :=
-lim_eq_of_equiv_const $ setoid.refl _
-
-lemma lim_add (f g : cau_seq ℝ abs) : lim f + lim g = lim ⇑(f + g) :=
-eq_lim_of_const_equiv $ show lim_zero (const abs (lim ⇑f + lim ⇑g) - (f + g)),
-  by rw [const_add, add_sub_comm];
-  exact add_lim_zero (setoid.symm (equiv_lim f)) (setoid.symm (equiv_lim g))
-
-lemma lim_mul_lim (f g : cau_seq ℝ abs) : lim f * lim g = lim ⇑(f * g) :=
-eq_lim_of_const_equiv $ show lim_zero (const abs (lim ⇑f * lim ⇑g) - f * g),
-  from have h : const abs (lim ⇑f * lim ⇑g) - f * g = g * (const abs (lim f) - f)
-      + const abs (lim f) * (const abs (lim g) - g) :=
-    by simp [mul_sub, mul_comm, const_mul, mul_add],
-  by rw h; exact add_lim_zero (mul_lim_zero _ (setoid.symm (equiv_lim f)))
-      (mul_lim_zero _ (setoid.symm (equiv_lim g)))
-
-lemma lim_mul (f : cau_seq ℝ abs) (x : ℝ) : lim f * x = lim ⇑(f * const abs x) :=
-by rw [← lim_mul_lim, lim_const]
-
-lemma lim_neg (f : cau_seq ℝ abs) : lim ⇑(-f) = -lim f :=
-lim_eq_of_equiv_const (show lim_zero (-f - const abs (-lim ⇑f)),
-  by rw [const_neg, sub_neg_eq_add, add_comm];
-  exact setoid.symm (equiv_lim f))
-
-lemma lim_eq_zero_iff (f : cau_seq ℝ abs) : lim f = 0 ↔ lim_zero f :=
-⟨assume h,
-  by have hf := equiv_lim f;
-  rw h at hf;
-  exact (lim_zero_congr hf).mpr (const_lim_zero.mpr rfl),
-assume h,
-  have h₁ : f = (f - const abs 0) := ext (λ n, by simp [sub_apply, const_apply]),
-  by rw h₁ at h; exact lim_eq_of_equiv_const h ⟩
-
-lemma lim_inv {f : cau_seq ℝ abs} (hf : ¬ lim_zero f) : lim ⇑(inv f hf) = (lim f)⁻¹ :=
-have hl : lim f ≠ 0 := by rwa ← lim_eq_zero_iff at hf,
-lim_eq_of_equiv_const $ show lim_zero (inv f hf - const abs (lim ⇑f)⁻¹),
-  from have h₁ : ∀ (g f : cau_seq ℝ abs) (hf : ¬ lim_zero f), lim_zero (g - f * inv f hf * g) :=
-    λ g f hf, by rw [← one_mul g, ← mul_assoc, ← sub_mul, mul_one, mul_comm, mul_comm f];
-    exact mul_lim_zero _ (setoid.symm (cau_seq.inv_mul_cancel _)),
-  have h₂ : lim_zero ((inv f hf - const abs (lim ⇑f)⁻¹) - (const abs (lim f) - f) *
-      (inv f hf * const abs (lim ⇑f)⁻¹)) :=
-    by rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add];
-    exact show lim_zero (inv f hf - const abs (lim ⇑f) * (inv f hf * const abs (lim ⇑f)⁻¹)
-      - (const abs (lim ⇑f)⁻¹ - f * (inv f hf * const abs (lim ⇑f)⁻¹))),
-    from sub_lim_zero
-      (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _)
-      (by rw [← mul_assoc]; exact h₁ _ _ _),
-  (lim_zero_congr h₂).mpr $ by rw mul_comm; exact mul_lim_zero _ (setoid.symm (equiv_lim f))
-
-lemma lim_le {f : cau_seq ℝ abs} {x : ℝ}
-  (h : f ≤ cau_seq.const abs x) : real.lim f ≤ x :=
-cau_seq.const_le.1 $ cau_seq.le_of_eq_of_le (setoid.symm (real.equiv_lim f)) h
-
-lemma le_lim {f : cau_seq ℝ abs} {x : ℝ}
-  (h : cau_seq.const abs x ≤ f) : x ≤ real.lim f :=
-cau_seq.const_le.1 $ cau_seq.le_of_le_of_eq h (real.equiv_lim f)
-
-lemma lt_lim {f : cau_seq ℝ abs} {x : ℝ}
-  (h : cau_seq.const abs x < f) : x < real.lim f :=
-cau_seq.const_lt.1 $ cau_seq.lt_of_lt_of_eq h (real.equiv_lim f)
-
-lemma lim_lt {f : cau_seq ℝ abs} {x : ℝ}
-  (h : f < cau_seq.const abs x) : real.lim f < x :=
-cau_seq.const_lt.1 $ cau_seq.lt_of_eq_of_lt (setoid.symm (real.equiv_lim f)) h
-
-end lim
+noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
 
 theorem sqrt_exists : ∀ {x : ℝ}, 0 ≤ x → ∃ y, 0 ≤ y ∧ y * y = x :=
 suffices H : ∀ {x : ℝ}, 0 < x → x ≤ 1 → ∃ y, 0 < y ∧ y * y = x, begin