chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648)

These don't have a preferred direction, but there are cases when they are definitely needed.

The conversion paths commute as squares:
```
`→+` <-- `→+*` <-- `→ₐ[R]`
 ^         ^          ^
 |         |          |
`≃+` <-- `≃+*` <-- `≃ₐ[R]`
```
so we only need lemmas to swap within each square.

src/algebra/algebra/basic.lean

@@ -723,6 +723,10 @@ instance has_coe_to_alg_hom : has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂
 @[simp, norm_cast] lemma coe_alg_hom : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e :=
 rfl
 
+/-- The two paths coercion can take to a `ring_hom` are equivalent -/
+lemma coe_ring_hom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) :=
+rfl
+
 @[simp] lemma map_pow : ∀ (x : A₁) (n : ℕ), e (x ^ n) = (e x) ^ n := e.to_alg_hom.map_pow
 
 lemma injective : function.injective e := e.to_equiv.injective

src/algebra/module/linear_map.lean

@@ -446,6 +446,11 @@ def trans : M ≃ₗ[R] M₃ :=
 
 @[simp] lemma coe_to_add_equiv : ⇑(e.to_add_equiv) = e := rfl
 
+/-- The two paths coercion can take to an `add_monoid_hom` are equivalent -/
+lemma to_add_monoid_hom_commutes :
+  e.to_linear_map.to_add_monoid_hom = e.to_add_equiv.to_add_monoid_hom :=
+rfl
+
 @[simp] theorem trans_apply (c : M) :
   (e₁.trans e₂) c = e₂ (e₁ c) := rfl
 @[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.6 c

src/data/equiv/ring.lean

@@ -256,6 +256,21 @@ abbreviation to_monoid_hom (e : R ≃+* S) : R →* S := e.to_ring_hom.to_monoid
 /-- Reinterpret a ring equivalence as an `add_monoid` homomorphism. -/
 abbreviation to_add_monoid_hom (e : R ≃+* S) : R →+ S := e.to_ring_hom.to_add_monoid_hom
 
+/-- The two paths coercion can take to an `add_monoid_hom` are equivalent -/
+lemma to_add_monoid_hom_commutes (f : R ≃+* S) :
+  (f : R →+* S).to_add_monoid_hom = (f : R ≃+ S).to_add_monoid_hom :=
+rfl
+
+/-- The two paths coercion can take to an `monoid_hom` are equivalent -/
+lemma to_monoid_hom_commutes (f : R ≃+* S) :
+  (f : R →+* S).to_monoid_hom = (f : R ≃* S).to_monoid_hom :=
+rfl
+
+/-- The two paths coercion can take to an `equiv` are equivalent -/
+lemma to_equiv_commutes (f : R ≃+* S) :
+  (f : R ≃+ S).to_equiv = (f : R ≃* S).to_equiv :=
+rfl
+
 @[simp]
 lemma to_ring_hom_refl : (ring_equiv.refl R).to_ring_hom = ring_hom.id R := rfl