diff --git a/src/data/real/cau_seq.lean b/src/data/real/cau_seq.lean
index 205e834413fa5..6d5d9ec430435 100644
--- a/src/data/real/cau_seq.lean
+++ b/src/data/real/cau_seq.lean
@@ -321,20 +321,14 @@ instance equiv : setoid (cau_seq β abv) :=
 
 lemma add_equiv_add {f1 f2 g1 g2 : cau_seq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
   f1 + g1 ≈ f2 + g2 :=
-begin
-  change lim_zero ((f1 + g1) - _),
-  convert add_lim_zero hf hg using 1,
-  simp only [sub_eq_add_neg, add_assoc],
-  rw add_comm (-f2), simp only [add_assoc],
-  congr' 2, simp
-end
+by simpa only [←add_sub_add_comm] using add_lim_zero hf hg
 
 lemma neg_equiv_neg {f g : cau_seq β abv} (hf : f ≈ g) : -f ≈ -g :=
-begin
-  show lim_zero (-f - -g),
-  rw ←neg_sub',
-  exact neg_lim_zero hf,
-end
+by simpa only [neg_sub'] using neg_lim_zero hf
+
+lemma sub_equiv_sub {f1 f2 g1 g2 : cau_seq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
+  f1 - g1 ≈ f2 - g2 :=
+by simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)
 
 theorem equiv_def₃ {f g : cau_seq β abv} (h : f ≈ g) {ε : α} (ε0 : 0 < ε) :
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
@@ -417,6 +411,11 @@ variables {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
 lemma mul_equiv_zero' (g : cau_seq _ abv) {f : cau_seq _ abv} (hf : f ≈ 0) : f * g ≈ 0 :=
 by rw mul_comm; apply mul_equiv_zero _ hf
 
+lemma mul_equiv_mul {f1 f2 g1 g2 : cau_seq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
+  f1 * g1 ≈ f2 * g2 :=
+by simpa only [mul_sub, mul_comm, sub_add_sub_cancel]
+  using add_lim_zero (mul_lim_zero_right g1 hf) (mul_lim_zero_right f2 hg)
+
 end comm_ring
 
 section is_domain
diff --git a/src/data/real/cau_seq_completion.lean b/src/data/real/cau_seq_completion.lean
index 30c208f6672bf..d0f1dfc984bfc 100644
--- a/src/data/real/cau_seq_completion.lean
+++ b/src/data/real/cau_seq_completion.lean
@@ -44,32 +44,22 @@ by have : mk f = 0 ↔ lim_zero (f - 0) := quotient.eq;
    rwa sub_zero at this
 
 instance : has_add Cauchy :=
-⟨λ x y, quotient.lift_on₂ x y (λ f g, mk (f + g)) $
-  λ f₁ g₁ f₂ g₂ hf hg, quotient.sound $
-  by simpa [(≈), setoid.r, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
-    using add_lim_zero hf hg⟩
+⟨quotient.map₂ (+) $ λ f₁ g₁ hf f₂ g₂ hg, add_equiv_add hf hg⟩
 
 @[simp] theorem mk_add (f g : cau_seq β abv) : mk f + mk g = mk (f + g) := rfl
 
 instance : has_neg Cauchy :=
-⟨λ x, quotient.lift_on x (λ f, mk (-f)) $
-  λ f₁ f₂ hf, quotient.sound $
-  by simpa [neg_sub', (≈), setoid.r] using neg_lim_zero hf⟩
+⟨quotient.map has_neg.neg $ λ f₁ f₂ hf, neg_equiv_neg hf⟩
 
 @[simp] theorem mk_neg (f : cau_seq β abv) : -mk f = mk (-f) := rfl
 
 instance : has_mul Cauchy :=
-⟨λ x y, quotient.lift_on₂ x y (λ f g, mk (f * g)) $
-  λ f₁ g₁ f₂ g₂ hf hg, quotient.sound $
-  by simpa [(≈), setoid.r, mul_add, mul_comm, add_assoc, sub_eq_add_neg] using
-    add_lim_zero (mul_lim_zero_right g₁ hf) (mul_lim_zero_right f₂ hg)⟩
+⟨quotient.map₂ (*) $ λ f₁ g₁ hf f₂ g₂ hg, mul_equiv_mul hf hg⟩
 
 @[simp] theorem mk_mul (f g : cau_seq β abv) : mk f * mk g = mk (f * g) := rfl
 
 instance : has_sub Cauchy :=
-⟨λ x y, quotient.lift_on₂ x y (λ f g, mk (f - g)) $
-  λ f₁ g₁ f₂ g₂ hf hg, quotient.sound $ show ((f₁ - g₁) - (f₂ - g₂)).lim_zero,
-    by simpa [sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using sub_lim_zero hf hg⟩
+⟨quotient.map₂ has_sub.sub $ λ f₁ g₁ hf f₂ g₂ hg, sub_equiv_sub hf hg⟩
 
 @[simp] theorem mk_sub (f g : cau_seq β abv) : mk f - mk g = mk (f - g) := rfl