diff --git a/src/algebra/hom/equiv.lean b/src/algebra/hom/equiv.lean
index 6c97f007cdda4..6cd2f66b0249a 100644
--- a/src/algebra/hom/equiv.lean
+++ b/src/algebra/hom/equiv.lean
@@ -297,6 +297,22 @@ e.to_equiv.eq_symm_apply
 @[to_additive] lemma symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
   e.symm ∘ g = f ↔ g = e ∘ f := e.to_equiv.symm_comp_eq f g
 
+@[simp, to_additive]
+theorem symm_trans_self (e : M ≃* N) : e.symm.trans e = refl N :=
+fun_like.ext _ _ e.apply_symm_apply
+
+@[simp, to_additive]
+theorem self_trans_symm (e : M ≃* N) : e.trans e.symm = refl M :=
+fun_like.ext _ _ e.symm_apply_apply
+
+@[to_additive, simp] lemma coe_monoid_hom_refl {M} [mul_one_class M] :
+  (refl M : M →* M) = monoid_hom.id M := rfl
+
+@[to_additive, simp] lemma coe_monoid_hom_trans {M N P}
+  [mul_one_class M] [mul_one_class N] [mul_one_class P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
+  (e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ :=
+rfl
+
 /-- Two multiplicative isomorphisms agree if they are defined by the
     same underlying function. -/
 @[ext, to_additive
diff --git a/src/algebra/ring/equiv.lean b/src/algebra/ring/equiv.lean
index 207189ee280a7..cb682e18ebac1 100644
--- a/src/algebra/ring/equiv.lean
+++ b/src/algebra/ring/equiv.lean
@@ -207,13 +207,19 @@ symm_bijective.injective $ ext $ λ x, rfl
 @[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
 { .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) }
 
-@[simp] lemma trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :
+lemma trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :
   e₁.trans e₂ a = e₂ (e₁ a) := rfl
 
+@[simp] lemma coe_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R → S') = e₂ ∘ e₁ := rfl
+
 @[simp]
 lemma symm_trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') :
   (e₁.trans e₂).symm a = e₁.symm (e₂.symm a) := rfl
 
+lemma symm_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂).symm = e₂.symm.trans (e₁.symm) := rfl
+
 protected lemma bijective (e : R ≃+* S) : function.bijective e := equiv_like.bijective e
 protected lemma injective (e : R ≃+* S) : function.injective e := equiv_like.injective e
 protected lemma surjective (e : R ≃+* S) : function.surjective e := equiv_like.surjective e
@@ -224,6 +230,11 @@ protected lemma surjective (e : R ≃+* S) : function.surjective e := equiv_like
 lemma image_eq_preimage (e : R ≃+* S) (s : set R) : e '' s = e.symm ⁻¹' s :=
 e.to_equiv.image_eq_preimage s
 
+@[simp] lemma coe_mul_equiv_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R ≃* S') = (e₁ : R ≃* S).trans ↑e₂:= rfl
+@[simp] lemma coe_add_equiv_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R ≃+ S') = (e₁ : R ≃+ S).trans ↑e₂:= rfl
+
 end basic
 
 section opposite
@@ -335,6 +346,21 @@ protected lemma map_eq_one_iff : f x = 1 ↔ x = 1 := mul_equiv_class.map_eq_one
 
 lemma map_ne_one_iff : f x ≠ 1 ↔ x ≠ 1 := mul_equiv_class.map_ne_one_iff f
 
+lemma coe_monoid_hom_refl : (ring_equiv.refl R : R →* R) = monoid_hom.id R := rfl
+@[simp] lemma coe_add_monoid_hom_refl : (ring_equiv.refl R : R →+ R) = add_monoid_hom.id R := rfl
+/-! `ring_equiv.coe_mul_equiv_refl` and `ring_equiv.coe_add_equiv_refl` are proved above
+in higher generality -/
+@[simp] lemma coe_ring_hom_refl : (ring_equiv.refl R : R →* R) = ring_hom.id R := rfl
+
+@[simp] lemma coe_monoid_hom_trans [non_assoc_semiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R →* S') = (e₂ : S →* S').comp ↑e₁ := rfl
+@[simp] lemma coe_add_monoid_hom_trans [non_assoc_semiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R →+ S') = (e₂ : S →+ S').comp ↑e₁ := rfl
+/-! `ring_equiv.coe_mul_equiv_trans` and `ring_equiv.coe_add_equiv_trans` are proved above
+in higher generality -/
+@[simp] lemma coe_ring_hom_trans [non_assoc_semiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+  (e₁.trans e₂ : R →+* S') = (e₂ : S →+* S').comp ↑e₁ := rfl
+
 end semiring
 
 section non_unital_ring