feat(algebra/*): coe_to_equiv_symm simp lemmas (#12996)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/algebra/basic.lean

@@ -814,6 +814,8 @@ rfl
 
 @[simp] lemma to_fun_eq_coe (e : A₁ ≃ₐ[R] A₂) : e.to_fun = e := rfl
 
+@[simp] lemma to_equiv_eq_coe : e.to_equiv = e := rfl
+
 @[simp] lemma to_ring_equiv_eq_coe : e.to_ring_equiv = e := rfl
 
 @[simp, norm_cast] lemma coe_ring_equiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl

src/algebra/hom/equiv.lean

@@ -149,11 +149,14 @@ instance [has_mul M] [has_mul N] : mul_equiv_class (M ≃* N) M N :=
 
 variables [has_mul M] [has_mul N] [has_mul P] [has_mul Q]
 
+@[simp, to_additive]
+lemma to_equiv_eq_coe (f : M ≃* N) : f.to_equiv = f := rfl
+
 @[simp, to_additive]
 lemma to_fun_eq_coe {f : M ≃* N} : f.to_fun = f := rfl
 
 @[simp, to_additive]
-lemma coe_to_equiv {f : M ≃* N} : ⇑f.to_equiv = f := rfl
+lemma coe_to_equiv {f : M ≃* N} : ⇑(f : M ≃ N) = f := rfl
 
 @[simp, to_additive]
 lemma coe_to_mul_hom {f : M ≃* N} : ⇑f.to_mul_hom = f := rfl

src/algebra/module/equiv.lean

@@ -178,6 +178,8 @@ include σ'
 @[simp] lemma inv_fun_eq_symm : e.inv_fun = e.symm := rfl
 omit σ'
 
+@[simp] lemma coe_to_equiv_symm : ⇑e.to_equiv.symm = e.symm := rfl
+
 variables {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃}
 variables {module_N₁ : module R₁ N₁} {module_N₂ : module R₁ N₂}
 variables {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}

src/group_theory/commensurable.lean

@@ -53,10 +53,10 @@ lemma equivalence : equivalence (@commensurable G _) :=
 /--Equivalence of `K/H ⊓ K` with `gKg⁻¹/gHg⁻¹ ⊓ gKg⁻¹`-/
 def  quot_conj_equiv (H K : subgroup G) (g : conj_act G) :
   K ⧸ (H.subgroup_of K) ≃ (g • K).1 ⧸ ((g • H).subgroup_of (g • K)) :=
-quotient.congr (K.equiv_smul g).to_equiv (λ a b, by rw [←quotient.eq', ←quotient.eq',
+quotient.congr (K.equiv_smul g).to_equiv (λ a b, by { rw [←quotient.eq', ←quotient.eq',
   quotient_group.eq', quotient_group.eq', subgroup.mem_subgroup_of, subgroup.mem_subgroup_of,
-  mul_equiv.coe_to_equiv, ←mul_equiv.map_inv, ←mul_equiv.map_mul,
-  subgroup.equiv_smul_apply_coe, subgroup.smul_mem_pointwise_smul_iff])
+  mul_equiv.to_equiv_eq_coe, mul_equiv.coe_to_equiv, ←mul_equiv.map_inv, ←mul_equiv.map_mul,
+  subgroup.equiv_smul_apply_coe, subgroup.smul_mem_pointwise_smul_iff] })
 
 lemma commensurable_conj {H K : subgroup G} (g : conj_act G) :
    commensurable H K ↔ commensurable (g • H) (g • K) :=