chore(data/equiv/*): add missing coercion lemmas for equivs (#6268)

This does not affect the simp-normal form.

This tries to make a lot of lemma names and statements more consistent:
* restates `linear_map.mk_apply` to be `linear_map.coe_mk` to match `monoid_hom.coe_mk`
* adds `linear_map.to_linear_map_eq_coe`
* adds the simp lemma `linear_map.coe_to_equiv`
* adds the simp lemma `linear_map.linear_map.coe_to_linear_map`
* adds the simp lemma `linear_map.to_fun_eq_coe`
* adds the missing `ancestor` attributes required to make `to_additive` work for things like `add_equiv.to_add_hom`
* restates `add_equiv.to_fun_apply` to be `add_equiv.to_fun_eq_coe`
* restates `add_equiv.to_equiv_apply` to be `add_equiv.coe_to_equiv`
* adds the simp lemma `add_equiv.coe_to_mul_hom`
* removes `add_equiv.to_add_monoid_hom_apply` since `add_equiv.coe_to_add_monoid_hom` is a shorter and more general statement
* restates `ring_equiv.to_fun_apply` to be `ring_equiv.to_fun_eq_coe`
* restates `ring_equiv.coe_mul_equiv` to be `ring_equiv.coe_to_mul_equiv`
* restates `ring_equiv.coe_add_equiv` to be `ring_equiv.coe_to_add_equiv`
* restates `ring_equiv.coe_ring_hom` to be `ring_equiv.coe_to_ring_hom`
* adds `ring_equiv.to_ring_hom_eq_coe`
* adds `ring_equiv.to_add_equiv_eq_coe`
* adds `ring_equiv.to_mul_equiv_eq_coe`

src/algebra/group/hom.lean

@@ -72,6 +72,7 @@ structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=
 (map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)
 
 /-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/
+@[ancestor zero_hom add_hom]
 structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N]
   extends zero_hom M N, add_hom M N
 
@@ -93,16 +94,17 @@ structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
 (map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)
 
 /-- Bundled monoid homomorphisms; use this for bundled group homomorphisms too. -/
-@[to_additive]
+@[ancestor one_hom mul_hom, to_additive]
 structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] extends one_hom M N, mul_hom M N
 
 /-- Bundled monoid with zero homomorphisms; use this for bundled group with zero homomorphisms
 too. -/
+@[ancestor zero_hom monoid_hom]
 structure monoid_with_zero_hom (M : Type*) (N : Type*) [monoid_with_zero M] [monoid_with_zero N]
   extends zero_hom M N, monoid_hom M N
 
-attribute [nolint doc_blame, to_additive] monoid_hom.to_mul_hom
-attribute [nolint doc_blame, to_additive] monoid_hom.to_one_hom
+attribute [nolint doc_blame] monoid_hom.to_mul_hom
+attribute [nolint doc_blame] monoid_hom.to_one_hom
 attribute [nolint doc_blame] monoid_with_zero_hom.to_monoid_hom
 attribute [nolint doc_blame] monoid_with_zero_hom.to_zero_hom
 

src/algebra/lie/matrix.lean

@@ -70,7 +70,7 @@ types is an equivalence of Lie algebras. -/
 def matrix.reindex_lie_equiv {m : Type w₁} [decidable_eq m] [fintype m]
   (e : n ≃ m) : matrix n n R ≃ₗ⁅R⁆ matrix m m R :=
 { map_lie' := λ M N, by simp only [lie_ring.of_associative_ring_bracket, matrix.reindex_mul,
-    matrix.mul_eq_mul, linear_equiv.map_sub, linear_equiv.to_fun_apply],
+    matrix.mul_eq_mul, linear_equiv.map_sub, linear_equiv.to_fun_eq_coe],
 ..(matrix.reindex_linear_equiv e e) }
 
 @[simp] lemma matrix.reindex_lie_equiv_apply {m : Type w₁} [decidable_eq m] [fintype m]

src/algebra/module/linear_map.lean

@@ -354,8 +354,8 @@ instance : has_coe (M ≃ₗ[R] M₂) (M →ₗ[R] M₂) := ⟨to_linear_map⟩
 -- see Note [function coercion]
 instance : has_coe_to_fun (M ≃ₗ[R] M₂) := ⟨_, λ f, f.to_fun⟩
 
-@[simp] lemma mk_apply {to_fun inv_fun map_add map_smul left_inv right_inv  a} :
-  (⟨to_fun, map_add, map_smul, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂) a = to_fun a :=
+@[simp] lemma coe_mk {to_fun inv_fun map_add map_smul left_inv right_inv } :
+  ⇑(⟨to_fun, map_add, map_smul, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂) = to_fun :=
 rfl
 
 -- This exists for compatibility, previously `≃ₗ[R]` extended `≃` instead of `≃+`.
@@ -381,11 +381,15 @@ section
 variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂}
 variables (e e' : M ≃ₗ[R] M₂)
 
-@[simp, norm_cast] theorem coe_coe : ((e : M →ₗ[R] M₂) : M → M₂) = (e : M → M₂) := rfl
+lemma to_linear_map_eq_coe : e.to_linear_map = ↑e := rfl
 
-@[simp] lemma coe_to_equiv : (e.to_equiv : M → M₂) = (e : M → M₂) := rfl
+@[simp, norm_cast] theorem coe_coe : ⇑(e : M →ₗ[R] M₂) = e := rfl
 
-@[simp] lemma to_fun_apply {m : M} : e.to_fun m = e m := rfl
+@[simp] lemma coe_to_equiv : ⇑e.to_equiv = e := rfl
+
+@[simp] lemma coe_to_linear_map : ⇑e.to_linear_map = e := rfl
+
+@[simp] lemma to_fun_eq_coe : e.to_fun = e := rfl
 
 section
 variables {e e'}

src/algebra/quandle.lean

@@ -310,7 +310,7 @@ def conj (G : Type*) := G
 instance conj.quandle (G : Type*) [group G] : quandle (conj G) :=
 { act := (λ x, @mul_aut.conj G _ x),
   self_distrib := λ x y z, begin
-    dsimp only [mul_equiv.to_equiv_apply, mul_aut.conj_apply, conj],
+    dsimp only [mul_equiv.coe_to_equiv, mul_aut.conj_apply, conj],
     group,
   end,
   inv_act := (λ x, (@mul_aut.conj G _ x).symm),

src/data/equiv/mul_add.lean

@@ -37,6 +37,7 @@ variables {A : Type*} {B : Type*} {M : Type*} {N : Type*}
 set_option old_structure_cmd true
 
 /-- add_equiv α β is the type of an equiv α ≃ β which preserves addition. -/
+@[ancestor equiv add_hom]
 structure add_equiv (A B : Type*) [has_add A] [has_add B] extends A ≃ B, add_hom A B
 
 /-- The `equiv` underlying an `add_equiv`. -/
@@ -45,7 +46,7 @@ add_decl_doc add_equiv.to_equiv
 add_decl_doc add_equiv.to_add_hom
 
 /-- `mul_equiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
-@[to_additive]
+@[ancestor equiv mul_hom, to_additive]
 structure mul_equiv (M N : Type*) [has_mul M] [has_mul N] extends M ≃ N, mul_hom M N
 
 /-- The `equiv` underlying a `mul_equiv`. -/
@@ -64,10 +65,13 @@ instance [has_mul M] [has_mul N] : has_coe_to_fun (M ≃* N) := ⟨_, mul_equiv.
 variables [has_mul M] [has_mul N] [has_mul P] [has_mul Q]
 
 @[simp, to_additive]
-lemma to_fun_apply {f : M ≃* N} {m : M} : f.to_fun m = f m := rfl
+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
 
 @[simp, to_additive]
-lemma to_equiv_apply {f : M ≃* N} {m : M} : f.to_equiv m = f m := rfl
+lemma coe_to_mul_hom {f : M ≃* N} : ⇑f.to_mul_hom = f := rfl
 
 /-- A multiplicative isomorphism preserves multiplication (canonical form). -/
 @[simp, to_additive]
@@ -238,11 +242,6 @@ lemma coe_to_monoid_hom {M N} [monoid M] [monoid N] (e : M ≃* N) :
   ⇑e.to_monoid_hom = e :=
 rfl
 
-@[to_additive]
-lemma to_monoid_hom_apply {M N} [monoid M] [monoid N] (e : M ≃* N) (x : M) :
-  e.to_monoid_hom x = e x :=
-rfl
-
 @[to_additive] lemma to_monoid_hom_injective
   {M N} [monoid M] [monoid N] : function.injective (to_monoid_hom : (M ≃* N) → M →* N) :=
 λ f g h, mul_equiv.ext (monoid_hom.ext_iff.1 h)

src/data/equiv/ring.lean

@@ -62,7 +62,7 @@ variables [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add
 
 instance : has_coe_to_fun (R ≃+* S) := ⟨_, ring_equiv.to_fun⟩
 
-@[simp] lemma to_fun_eq_coe_fun (f : R ≃+* S) : f.to_fun = f := rfl
+@[simp] lemma to_fun_eq_coe (f : R ≃+* S) : f.to_fun = f := rfl
 
 /-- A ring isomorphism preserves multiplication. -/
 @[simp] lemma map_mul (e : R ≃+* S) (x y : R) : e (x * y) = e x * e y := e.map_mul' x y
@@ -92,11 +92,13 @@ instance has_coe_to_mul_equiv : has_coe (R ≃+* S) (R ≃* S) := ⟨ring_equiv.
 
 instance has_coe_to_add_equiv : has_coe (R ≃+* S) (R ≃+ S) := ⟨ring_equiv.to_add_equiv⟩
 
-@[norm_cast] lemma coe_mul_equiv (f : R ≃+* S) (a : R) :
-  (f : R ≃* S) a = f a := rfl
+lemma to_add_equiv_eq_coe (f : R ≃+* S) : f.to_add_equiv = ↑f := rfl
 
-@[norm_cast] lemma coe_add_equiv (f : R ≃+* S) (a : R) :
-  (f : R ≃+ S) a = f a := rfl
+lemma to_mul_equiv_eq_coe (f : R ≃+* S) : f.to_mul_equiv = ↑f := rfl
+
+@[simp, norm_cast] lemma coe_to_mul_equiv (f : R ≃+* S) : ⇑(f : R ≃* S) = f := rfl
+
+@[simp, norm_cast] lemma coe_to_add_equiv (f : R ≃+* S) : ⇑(f : R ≃+ S) = f := rfl
 
 /-- The `ring_equiv` between two semirings with a unique element. -/
 def ring_equiv_of_unique_of_unique {M N}
@@ -225,8 +227,9 @@ lemma to_ring_hom_injective : function.injective (to_ring_hom : (R ≃+* S) →
 
 instance has_coe_to_ring_hom : has_coe (R ≃+* S) (R →+* S) := ⟨ring_equiv.to_ring_hom⟩
 
-@[norm_cast] lemma coe_ring_hom (f : R ≃+* S) (a : R) :
-  (f : R →+* S) a = f a := rfl
+lemma to_ring_hom_eq_coe (f : R ≃+* S) : f.to_ring_hom = ↑f := rfl
+
+@[simp, norm_cast] lemma coe_to_ring_hom (f : R ≃+* S) : ⇑(f : R →+* S) = f := rfl
 
 lemma coe_ring_hom_inj_iff {R S : Type*} [semiring R] [semiring S] (f g : R ≃+* S) :
   f = g ↔ (f : R →+* S) = g :=

src/data/mv_polynomial/equiv.lean

@@ -261,10 +261,10 @@ lemma fin_succ_equiv_eq (n : ℕ) :
 begin
   apply ring_hom_ext,
   { intro r,
-    dsimp [ring_equiv.coe_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv],
+    dsimp [ring_equiv.coe_to_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv],
     simp only [sum_to_iter_C, eval₂_C, rename_C, ring_hom.coe_comp] },
   { intro i,
-    dsimp [ring_equiv.coe_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv,
+    dsimp [ring_equiv.coe_to_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv,
       _root_.fin_succ_equiv],
     by_cases hi : i = 0,
     { simp only [hi, fin.cases_zero, sum.swap, rename_X, equiv.option_equiv_sum_punit_none,

src/group_theory/semidirect_product.lean

@@ -160,7 +160,7 @@ def lift (f₁ : N →* H) (f₂ : G →* H)
   map_one' := by simp,
   map_mul' := λ a b, begin
     have := λ n g, monoid_hom.ext_iff.1 (h n) g,
-    simp only [mul_aut.conj_apply, monoid_hom.comp_apply, mul_equiv.to_monoid_hom_apply] at this,
+    simp only [mul_aut.conj_apply, monoid_hom.comp_apply, mul_equiv.coe_to_monoid_hom] at this,
     simp [this, mul_assoc]
   end }
 

src/linear_algebra/bilinear_form.lean

@@ -533,7 +533,7 @@ rfl
 begin
   ext i j,
   simp only [bilin_form.to_matrix'_apply, bilin_form.comp_apply, transpose_apply, matrix.mul_apply,
-    linear_map.to_matrix', linear_equiv.mk_apply, sum_mul],
+    linear_map.to_matrix', linear_equiv.coe_mk, sum_mul],
   rw sum_comm,
   conv_lhs { rw ← sum_repr_mul_repr_mul (pi.is_basis_fun R₃ n) (l _) (r _) },
   rw finsupp.sum_fintype,
@@ -661,7 +661,7 @@ lemma bilin_form.to_matrix_comp
 begin
   ext i j,
   simp only [bilin_form.to_matrix_apply, bilin_form.comp_apply, transpose_apply, matrix.mul_apply,
-    linear_map.to_matrix', linear_equiv.mk_apply, sum_mul],
+    linear_map.to_matrix', linear_equiv.coe_mk, sum_mul],
   rw sum_comm,
   conv_lhs { rw ← sum_repr_mul_repr_mul hb },
   rw finsupp.sum_fintype,

src/linear_algebra/matrix.lean

@@ -127,7 +127,7 @@ matrix.to_lin'.apply_symm_apply f
 @[simp] lemma linear_map.to_matrix'_apply (f : (n → R) →ₗ[R] (m → R)) (i j) :
   linear_map.to_matrix' f i j = f (λ j', if j' = j then 1 else 0) i :=
 begin
-  simp only [linear_map.to_matrix', linear_equiv.mk_apply],
+  simp only [linear_map.to_matrix', linear_equiv.coe_mk],
   congr,
   ext j',
   split_ifs with h,
@@ -762,7 +762,7 @@ end
 types is an equivalence of algebras. -/
 def reindex_alg_equiv [comm_semiring R] [decidable_eq m] [decidable_eq n]
   (e : m ≃ n) : matrix m m R ≃ₐ[R] matrix n n R :=
-{ map_mul'  := λ M N, by simp only [reindex_mul, linear_equiv.to_fun_apply, mul_eq_mul],
+{ map_mul'  := λ M N, by simp only [reindex_mul, linear_equiv.to_fun_eq_coe, mul_eq_mul],
   commutes' := λ r,
                  by { ext, simp [algebra_map, algebra.to_ring_hom], by_cases h : i = j; simp [h], },
 ..(reindex_linear_equiv e e) }

src/ring_theory/witt_vector/is_poly.lean

@@ -263,7 +263,7 @@ begin
   convert h,
   all_goals {
     funext i,
-    rw [← ring_equiv.coe_ring_hom],
+    rw [← ring_equiv.coe_to_ring_hom],
     simp only [hf, hg, mv_polynomial.eval, map_eval₂_hom],
     apply eval₂_hom_congr (ring_hom.ext_int _ _) _ rfl,
     ext1,
@@ -588,7 +588,7 @@ begin
   convert h; clear h,
   all_goals {
     funext i,
-    rw [← ring_equiv.coe_ring_hom],
+    rw [← ring_equiv.coe_to_ring_hom],
     simp only [hf, hg, mv_polynomial.eval, map_eval₂_hom],
     apply eval₂_hom_congr (ring_hom.ext_int _ _) _ rfl,
     ext1,