mathlib3

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

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`