diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 6aac166d8..611016a4a 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -121,12 +121,14 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)}
   (H : forall (r s : A) (H' : R r s), eq.drec_on (eq_abs Q H') (f r) = f s)
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
-have H2 [visible] : R a (rep (abs a)), from R_rep_abs Q Ha,
-let Heq : abs (rep (abs a)) = abs a := abs_rep Q (abs a) in
+have H2  [visible] : R a (rep (abs a)), from
+  R_rep_abs Q Ha,
+have Heq [visible] : abs (rep (abs a)) = abs a, from
+  abs_rep Q (abs a),
 calc
   rec Q f (abs a) =  eq.drec_on Heq (f (rep (abs a))) : rfl
-    ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹}
-    ... = f a : eq.rec_on_compose (eq_abs Q H2) _ _
+    ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a))   : {(H _ _ H2)⁻¹}
+    ... = f a                                         : eq.rec_on_compose (eq_abs Q H2) _ _
 
 definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=