diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 1cacf6da7..d4a38f3a9 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -208,7 +208,7 @@ theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
   fun_image f a = tag (f a) (exists.intro a rfl) := rfl
 
 theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a :=
-elt_of.tag _ _
+by esimp
 
 theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_of u :=
 has_property u
@@ -230,13 +230,13 @@ theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A)
 iff.intro
   (assume H : f a = f a', tag_eq H)
   (assume H : fun_image f a = fun_image f a',
-    (congr_arg elt_of H ▸ elt_of_fun_image f a) ▸ elt_of_fun_image f a')
+    by injection H; assumption)
 
 theorem idempotent_image_elt_of {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f)
   : fun_image f (elt_of u) = u :=
 obtain (a : A) (Ha : fun_image f a = u), from fun_image_surj u,
 calc
-  fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : {Ha⁻¹}
+  fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : by rewrite Ha
     ... = fun_image f (f a) : {elt_of_fun_image f a}
     ... = fun_image f a : {iff.elim_left (fun_image_eq f (f a) a) (H a)}
     ... = u : Ha
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index fa36ae7c9..898d9e564 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -48,10 +48,10 @@ namespace quotient
   (pr1.mk a a') ▸ (pr2.mk a a') ▸ rfl
 
   theorem map_pair_pr1 (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
-  !pr1.mk
+  by esimp
 
   theorem map_pair_pr2 (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
-  !pr2.mk
+  by esimp
 
   /- coordinatewise binary maps -/
 
@@ -72,10 +72,10 @@ namespace quotient
       ... = pair (f a b) (f a' b') : {pr1.mk a a'}
 
   theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-  pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.mk
+  pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := by esimp
 
   theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-  pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.mk
+  pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := by esimp
 
   theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
     flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
@@ -123,7 +123,7 @@ have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) =
           = f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _
       ... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _}
       ... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w)
-      ... = f (pr1 u) (pr1 (map_pair2 f v w)) : {(map_pair2_pr1 f _ _)⁻¹}
+      ... = f (pr1 u) (pr1 (map_pair2 f v w)) : by rewrite [map_pair2_pr1 f]
       ... = pr1 (map_pair2 f u (map_pair2 f v w)) : (map_pair2_pr1 f _ _)⁻¹,
 have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) =
           pr2 (map_pair2 f u (map_pair2 f v w)), from