diff --git a/src/category_theory/is_connected.lean b/src/category_theory/is_connected.lean
index cb0d41a403b53..a087eef022bf5 100644
--- a/src/category_theory/is_connected.lean
+++ b/src/category_theory/is_connected.lean
@@ -251,11 +251,7 @@ If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁`
 -/
 lemma zigzag_obj_of_zigzag (F : J ⥤ K) {j₁ j₂ : J} (h : zigzag j₁ j₂) :
   zigzag (F.obj j₁) (F.obj j₂) :=
-begin
-  refine relation.refl_trans_gen_lift _ _ h,
-  intros j k,
-  exact or.imp (nonempty.map (λ f, F.map f)) (nonempty.map (λ f, F.map f))
-end
+h.lift _ $ λ j k, or.imp (nonempty.map (λ f, F.map f)) (nonempty.map (λ f, F.map f))
 
 -- TODO: figure out the right way to generalise this to `zigzag`.
 lemma zag_of_zag_obj (F : J ⥤ K) [full F] {j₁ j₂ : J} (h : zag (F.obj j₁) (F.obj j₂)) :
diff --git a/src/category_theory/limits/types.lean b/src/category_theory/limits/types.lean
index 725f39a44564c..f26d80d8efccc 100644
--- a/src/category_theory/limits/types.lean
+++ b/src/category_theory/limits/types.lean
@@ -336,8 +336,8 @@ begin
   ext ⟨j, x⟩ ⟨j', y⟩,
   split,
   { apply eqv_gen_quot_rel_of_rel },
-  { rw ← relation.eqv_gen_iff_of_equivalence (filtered_colimit.rel_equiv F),
-    exact relation.eqv_gen_mono (rel_of_quot_rel F) }
+  { rw ←(filtered_colimit.rel_equiv F).eqv_gen_iff,
+    exact eqv_gen.mono (rel_of_quot_rel F) }
 end
 
 lemma colimit_eq_iff_aux {i j : J} {xi : F.obj i} {xj : F.obj j} :
diff --git a/src/data/pfunctor/multivariate/M.lean b/src/data/pfunctor/multivariate/M.lean
index aa4e27e061931..69e5a8dc3aa9a 100644
--- a/src/data/pfunctor/multivariate/M.lean
+++ b/src/data/pfunctor/multivariate/M.lean
@@ -260,8 +260,8 @@ begin
   replace h₁ := congr_fun (congr_fun h₁ fin2.fz) i,
   simp [(⊚),append_fun,split_fun] at h₁,
   replace h₁ := quot.exact _  h₁,
-  rw relation.eqv_gen_iff_of_equivalence at h₁,
-  exact h₁, exact h₀
+  rw h₀.eqv_gen_iff at h₁,
+  exact h₁,
 end
 
 theorem M.bisim' {α : typevec n} (R : P.M α → P.M α → Prop)
diff --git a/src/group_theory/free_group.lean b/src/group_theory/free_group.lean
index 5d64f7c3cd9bd..bf1a9fd72c30a 100644
--- a/src/group_theory/free_group.lean
+++ b/src/group_theory/free_group.lean
@@ -162,7 +162,7 @@ match b, c, red.step.diamond hab hac rfl with
 end)
 
 lemma cons_cons {p} : red L₁ L₂ → red (p :: L₁) (p :: L₂) :=
-refl_trans_gen_lift (list.cons p) (assume a b, step.cons)
+refl_trans_gen.lift (list.cons p) (assume a b, step.cons)
 
 lemma cons_cons_iff (p) : red (p :: L₁) (p :: L₂) ↔ red L₁ L₂ :=
 iff.intro
@@ -188,8 +188,7 @@ lemma append_append_left_iff : ∀L, red (L ++ L₁) (L ++ L₂) ↔ red L₁ L
 | (p :: L) := by simp [append_append_left_iff L, cons_cons_iff]
 
 lemma append_append (h₁ : red L₁ L₃) (h₂ : red L₂ L₄) : red (L₁ ++ L₂) (L₃ ++ L₄) :=
-(refl_trans_gen_lift (λL, L ++ L₂) (assume a b, step.append_right) h₁).trans
-  ((append_append_left_iff _).2 h₂)
+(h₁.lift (λL, L ++ L₂) (assume a b, step.append_right)).trans ((append_append_left_iff _).2 h₂)
 
 lemma to_append_iff : red L (L₁ ++ L₂) ↔ (∃L₃ L₄, L = L₃ ++ L₄ ∧ red L₃ L₁ ∧ red L₄ L₂) :=
 iff.intro
@@ -325,8 +324,8 @@ join_of_single reflexive_refl_trans_gen h.to_red
 theorem eqv_gen_step_iff_join_red : eqv_gen red.step L₁ L₂ ↔ join red L₁ L₂ :=
 iff.intro
   (assume h,
-    have eqv_gen (join red) L₁ L₂ := eqv_gen_mono (assume a b, join_red_of_step) h,
-    (eqv_gen_iff_of_equivalence $ equivalence_join_red).1 this)
+    have eqv_gen (join red) L₁ L₂ := h.mono (assume a b, join_red_of_step),
+    equivalence_join_red.eqv_gen_iff.1 this)
   (join_of_equivalence (eqv_gen.is_equivalence _) $ assume a b,
     refl_trans_gen_of_equivalence (eqv_gen.is_equivalence _) eqv_gen.rel)
 
diff --git a/src/logic/relation.lean b/src/logic/relation.lean
index 22efef5f2920f..cd7c93e0cb3c1 100644
--- a/src/logic/relation.lean
+++ b/src/logic/relation.lean
@@ -322,6 +322,10 @@ begin
     rcases IH with ⟨d, had, hdb⟩, exact ⟨_, had, hdb.tail hbc⟩ }
 end
 
+end trans_gen
+
+section trans_gen
+
 lemma trans_gen_eq_self (trans : transitive r) :
   trans_gen r = r :=
 funext $ λ a, funext $ λ b, propext $
@@ -333,13 +337,13 @@ end,
 trans_gen.single⟩
 
 lemma transitive_trans_gen : transitive (trans_gen r) :=
-λ a b c, trans
+λ a b c, trans_gen.trans
 
 lemma trans_gen_idem :
   trans_gen (trans_gen r) = trans_gen r :=
 trans_gen_eq_self transitive_trans_gen
 
-lemma trans_gen_lift {p : β → β → Prop} {a b : α} (f : α → β)
+lemma trans_gen.lift {p : β → β → Prop} {a b : α} (f : α → β)
   (h : ∀ a b, r a b → p (f a) (f b)) (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
 begin
   induction hab,
@@ -347,14 +351,14 @@ begin
   case trans_gen.tail : c d hac hcd hac { exact trans_gen.tail hac (h c d hcd) }
 end
 
-lemma trans_gen_lift' {p : β → β → Prop} {a b : α} (f : α → β)
+lemma trans_gen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
   (h : ∀ a b, r a b → trans_gen p (f a) (f b))
   (hab : trans_gen r a b) : trans_gen p (f a) (f b) :=
-by simpa [trans_gen_idem] using trans_gen_lift f h hab
+by simpa [trans_gen_idem] using hab.lift f h
 
-lemma trans_gen_closed {p : α → α → Prop} :
+lemma trans_gen.closed {p : α → α → Prop} :
   (∀ a b, r a b → trans_gen p a b) → trans_gen r a b → trans_gen p a b :=
-trans_gen_lift' id
+trans_gen.lift' id
 
 end trans_gen
 
@@ -374,14 +378,14 @@ begin
   { rcases h with rfl | h, {refl}, {exact h.to_refl} }
 end
 
-lemma refl_trans_gen_lift {p : β → β → Prop} {a b : α} (f : α → β)
+lemma refl_trans_gen.lift {p : β → β → Prop} {a b : α} (f : α → β)
   (h : ∀ a b, r a b → p (f a) (f b)) (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
 refl_trans_gen.trans_induction_on hab (λ a, refl)
   (λ a b, refl_trans_gen.single ∘ h _ _) (λ a b c _ _, trans)
 
-lemma refl_trans_gen_mono {p : α → α → Prop} :
+lemma refl_trans_gen.mono {p : α → α → Prop} :
   (∀ a b, r a b → p a b) → refl_trans_gen r a b → refl_trans_gen p a b :=
-refl_trans_gen_lift id
+refl_trans_gen.lift id
 
 lemma refl_trans_gen_eq_self (refl : reflexive r) (trans : transitive r) :
   refl_trans_gen r = r :=
@@ -401,14 +405,14 @@ lemma refl_trans_gen_idem :
   refl_trans_gen (refl_trans_gen r) = refl_trans_gen r :=
 refl_trans_gen_eq_self reflexive_refl_trans_gen transitive_refl_trans_gen
 
-lemma refl_trans_gen_lift' {p : β → β → Prop} {a b : α} (f : α → β)
+lemma refl_trans_gen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
   (h : ∀ a b, r a b → refl_trans_gen p (f a) (f b))
   (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
-by simpa [refl_trans_gen_idem] using refl_trans_gen_lift f h hab
+by simpa [refl_trans_gen_idem] using hab.lift f h
 
 lemma refl_trans_gen_closed {p : α → α → Prop} :
   (∀ a b, r a b → refl_trans_gen p a b) → refl_trans_gen r a b → refl_trans_gen p a b :=
-refl_trans_gen_lift' id
+refl_trans_gen.lift' id
 
 end refl_trans_gen
 
@@ -493,9 +497,13 @@ refl_trans_gen_of_transitive_reflexive hr.1 hr.2.2
 
 end join
 
+end relation
+
 section eqv_gen
 
-lemma eqv_gen_iff_of_equivalence (h : equivalence r) : eqv_gen r a b ↔ r a b :=
+variables {r : α → α → Prop} {a b : α}
+
+lemma equivalence.eqv_gen_iff (h : equivalence r) : eqv_gen r a b ↔ r a b :=
 iff.intro
   begin
     intro h,
@@ -507,7 +515,10 @@ iff.intro
   end
   (eqv_gen.rel a b)
 
-lemma eqv_gen_mono {r p : α → α → Prop}
+lemma equivalence.eqv_gen_eq (h : equivalence r) : eqv_gen r = r :=
+funext $ λ _, funext $ λ _, propext $ h.eqv_gen_iff
+
+lemma eqv_gen.mono {r p : α → α → Prop}
   (hrp : ∀ a b, r a b → p a b) (h : eqv_gen r a b) : eqv_gen p a b :=
 begin
   induction h,
@@ -517,9 +528,4 @@ begin
   case eqv_gen.trans : a b c ih1 ih2 hab hbc { exact eqv_gen.trans _ _ _ hab hbc }
 end
 
-lemma eqv_gen_eq_of_equivalence (h : equivalence r) : eqv_gen r = r :=
-funext $ λ _, funext $ λ _, propext $ eqv_gen_iff_of_equivalence h
-
 end eqv_gen
-
-end relation
diff --git a/test/qpf.lean b/test/qpf.lean
index b015723e205d6..f3a358092fb2e 100644
--- a/test/qpf.lean
+++ b/test/qpf.lean
@@ -102,8 +102,8 @@ by simp only [foo.mk, foo.map_mk]; refl
 lemma foo.map_tt {α : Type} (x y : α) :
   foo.mk tt x = foo.mk tt y ↔ x = y :=
 by simp [foo.mk]; split; intro h; [replace h := quot.exact _ h, rw h];
-   rw relation.eqv_gen_iff_of_equivalence at h;
-   [exact h.2 rfl, apply equivalence_foo.R]
+   rw (equivalence_foo.R _).eqv_gen_iff at h;
+   exact h.2 rfl
 
 /-- consequence of original definition of `supp`. If there exists more than
 one value of type `α`, then the support of `foo.mk ff x` is empty -/
@@ -157,7 +157,7 @@ begin
   { introv hp, simp [functor.liftp] at hp,
     rcases hp with ⟨⟨z,z',hz⟩,hp⟩,
     simp at hp, replace hp := quot.exact _ hp,
-    rw relation.eqv_gen_iff_of_equivalence (equivalence_foo.R _) at hp,
+    rw (equivalence_foo.R _).eqv_gen_iff at hp,
     rcases hp with ⟨⟨⟩,hp⟩, subst y,
     replace hp := hp rfl, cases hp,
     exact hz }