feat(data/equiv/mul_add): use @[simps] (#7213)

Add some `@[simps]` for some algebra maps. This came up in #6795.

src/algebra/group/hom.lean

@@ -363,20 +363,21 @@ let ⟨y, hy⟩ := hx in ⟨f y, f.map_mul_eq_one hy⟩
 end monoid_hom
 
 /-- The identity map from a type with 1 to itself. -/
-@[to_additive]
+@[to_additive, simps]
 def one_hom.id (M : Type*) [has_one M] : one_hom M M :=
-{ to_fun := id, map_one' := rfl, }
+{ to_fun := λ x, x, map_one' := rfl, }
 /-- The identity map from a type with multiplication to itself. -/
-@[to_additive]
+@[to_additive, simps]
 def mul_hom.id (M : Type*) [has_mul M] : mul_hom M M :=
-{ to_fun := id, map_mul' := λ _ _, rfl, }
+{ to_fun := λ x, x, map_mul' := λ _ _, rfl, }
 /-- The identity map from a monoid to itself. -/
-@[to_additive]
+@[to_additive, simps]
 def monoid_hom.id (M : Type*) [mul_one_class M] : M →* M :=
-{ to_fun := id, map_one' := rfl, map_mul' := λ _ _, rfl, }
+{ to_fun := λ x, x, map_one' := rfl, map_mul' := λ _ _, rfl, }
 /-- The identity map from a monoid_with_zero to itself. -/
+@[simps]
 def monoid_with_zero_hom.id (M : Type*) [mul_zero_one_class M] : monoid_with_zero_hom M M :=
-{ to_fun := id, map_zero' := rfl, map_one' := rfl, map_mul' := λ _ _, rfl, }
+{ to_fun := λ x, x, map_zero' := rfl, map_one' := rfl, map_mul' := λ _ _, rfl, }
 
 /-- The identity map from an type with zero to itself. -/
 add_decl_doc zero_hom.id
@@ -385,15 +386,6 @@ add_decl_doc add_hom.id
 /-- The identity map from an additive monoid to itself. -/
 add_decl_doc add_monoid_hom.id
 
-@[simp, to_additive] lemma one_hom.id_apply {M : Type*} [has_one M] (x : M) :
-  one_hom.id M x = x := rfl
-@[simp, to_additive] lemma mul_hom.id_apply {M : Type*} [has_mul M] (x : M) :
-  mul_hom.id M x = x := rfl
-@[simp, to_additive] lemma monoid_hom.id_apply {M : Type*} [mul_one_class M] (x : M) :
-  monoid_hom.id M x = x := rfl
-@[simp] lemma monoid_with_zero_hom.id_apply {M : Type*} [mul_zero_one_class M] (x : M) :
-  monoid_with_zero_hom.id M x = x := rfl
-
 /-- Composition of `one_hom`s as a `one_hom`. -/
 @[to_additive]
 def one_hom.comp [has_one M] [has_one N] [has_one P]
@@ -710,16 +702,13 @@ lemma injective_iff {G H} [group G] [mul_one_class H] (f : G →* H) :
 
 include mM
 /-- Makes a group homomorphism from a proof that the map preserves multiplication. -/
-@[to_additive "Makes an additive group homomorphism from a proof that the map preserves addition."]
+@[to_additive "Makes an additive group homomorphism from a proof that the map preserves addition.",
+  simps {fully_applied := ff}]
 def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G :=
 { to_fun := f,
   map_mul' := map_mul,
   map_one' := mul_left_eq_self.1 $ by rw [←map_mul, mul_one] }
 
-@[simp, to_additive]
-lemma coe_mk' {f : M → G} (map_mul : ∀ a b : M, f (a * b) = f a * f b) :
-  ⇑(mk' f map_mul) = f := rfl
-
 omit mM
 
 /-- Makes a group homomorphism from a proof that the map preserves right division `λ x y, x * y⁻¹`.

src/algebra/group/hom_instances.lean

@@ -72,12 +72,9 @@ rfl
 /-- Evaluation of a `monoid_hom` at a point as a monoid homomorphism. See also `monoid_hom.apply`
 for the evaluation of any function at a point. -/
 @[to_additive "Evaluation of an `add_monoid_hom` at a point as an additive monoid homomorphism.
-See also `add_monoid_hom.apply` for the evaluation of any function at a point."]
+See also `add_monoid_hom.apply` for the evaluation of any function at a point.", simps]
 def eval [mul_one_class M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id (M →* N)).flip
 
-@[simp, to_additive]
-lemma eval_apply [mul_one_class M] [comm_monoid N] (x : M) (f : M →* N) : eval x f = f x := rfl
-
 /-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
 @[to_additive "Composition of additive monoid morphisms
 (`add_monoid_hom.comp`) as an additive monoid morphism.", simps]

src/analysis/normed_space/normed_group_hom.lean

@@ -389,7 +389,7 @@ def comp_hom : (normed_group_hom V₂ V₃) →+ (normed_group_hom V₁ V₂) 
 add_monoid_hom.mk' (λ g, add_monoid_hom.mk' (λ f, g.comp f)
   (by { intros, ext, exact g.map_add _ _ }))
   (by { intros, ext, simp only [comp_apply, pi.add_apply, function.comp_app,
-                                add_monoid_hom.add_apply, add_monoid_hom.coe_mk', coe_add] })
+                                add_monoid_hom.add_apply, add_monoid_hom.mk'_apply, coe_add] })
 
 @[simp] lemma comp_zero (f : normed_group_hom V₂ V₃) : f.comp (0 : normed_group_hom V₁ V₂) = 0 :=
 by { ext, exact f.map_zero }

src/data/equiv/mul_add.lean

@@ -108,6 +108,7 @@ def refl (M : Type*) [has_mul M] : M ≃* M :=
 { map_mul' := λ _ _, rfl,
 ..equiv.refl _}
 
+@[to_additive]
 instance : inhabited (M ≃* M) := ⟨refl M⟩
 
 /-- The inverse of an isomorphism is an isomorphism. -/
@@ -343,7 +344,7 @@ def add_monoid_hom.to_add_equiv [add_zero_class M] [add_zero_class N] (f : M →
 /-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
 returns an multiplicative equivalence with `to_fun = f` and `inv_fun = g`.  This constructor is
 useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
-@[to_additive]
+@[to_additive, simps {fully_applied := ff}]
 def monoid_hom.to_mul_equiv [mul_one_class M] [mul_one_class N] (f : M →* N) (g : N →* M)
   (h₁ : g.comp f = monoid_hom.id _) (h₂ : f.comp g = monoid_hom.id _) :
   M ≃* N :=
@@ -353,18 +354,11 @@ def monoid_hom.to_mul_equiv [mul_one_class M] [mul_one_class N] (f : M →* N) (
   right_inv := monoid_hom.congr_fun h₂,
   map_mul' := f.map_mul }
 
-@[simp, to_additive]
-lemma monoid_hom.coe_to_mul_equiv [mul_one_class M] [mul_one_class N]
-  (f : M →* N) (g : N →* M) (h₁ h₂) :
-  ⇑(f.to_mul_equiv g h₁ h₂) = f := rfl
-
 /-- An additive equivalence of additive groups preserves subtraction. -/
 lemma add_equiv.map_sub [add_group A] [add_group B] (h : A ≃+ B) (x y : A) :
   h (x - y) = h x - h y :=
 h.to_add_monoid_hom.map_sub x y
 
-instance add_equiv.inhabited {M : Type*} [has_add M] : inhabited (M ≃+ M) := ⟨add_equiv.refl M⟩
-
 /-- A group is isomorphic to its group of units. -/
 @[to_additive to_add_units "An additive group is isomorphic to its group of additive units"]
 def to_units {G} [group G] : G ≃* units G :=
@@ -389,31 +383,27 @@ def map_equiv (h : M ≃* N) : units M ≃* units N :=
   .. map h.to_monoid_hom }
 
 /-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/
-@[to_additive "Left addition of an additive unit is a permutation of the underlying type."]
+@[to_additive "Left addition of an additive unit is a permutation of the underlying type.",
+  simps apply {fully_applied := ff}]
 def mul_left (u : units M) : equiv.perm M :=
 { to_fun    := λx, u * x,
   inv_fun   := λx, ↑u⁻¹ * x,
   left_inv  := u.inv_mul_cancel_left,
   right_inv := u.mul_inv_cancel_left }
 
-@[simp, to_additive]
-lemma coe_mul_left (u : units M) : ⇑u.mul_left = (*) u := rfl
-
 @[simp, to_additive]
 lemma mul_left_symm (u : units M) : u.mul_left.symm = u⁻¹.mul_left :=
 equiv.ext $ λ x, rfl
 
 /-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
-@[to_additive "Right addition of an additive unit is a permutation of the underlying type."]
+@[to_additive "Right addition of an additive unit is a permutation of the underlying type.",
+  simps apply {fully_applied := ff}]
 def mul_right (u : units M) : equiv.perm M :=
 { to_fun    := λx, x * u,
   inv_fun   := λx, x * ↑u⁻¹,
   left_inv  := λ x, mul_inv_cancel_right x u,
   right_inv := λ x, inv_mul_cancel_right x u }
 
-@[simp, to_additive]
-lemma coe_mul_right (u : units M) : ⇑u.mul_right = λ x : M, x * u := rfl
-
 @[simp, to_additive]
 lemma mul_right_symm (u : units M) : u.mul_right.symm = u⁻¹.mul_right :=
 equiv.ext $ λ x, rfl
@@ -460,7 +450,8 @@ attribute [nolint simp_nf] add_left_symm_apply add_right_symm_apply
 variable (G)
 
 /-- Inversion on a `group` is a permutation of the underlying type. -/
-@[to_additive "Negation on an `add_group` is a permutation of the underlying type."]
+@[to_additive "Negation on an `add_group` is a permutation of the underlying type.",
+  simps apply {fully_applied := ff}]
 protected def inv : perm G :=
 { to_fun    := λa, a⁻¹,
   inv_fun   := λa, a⁻¹,
@@ -469,9 +460,6 @@ protected def inv : perm G :=
 
 variable {G}
 
-@[simp, to_additive]
-lemma coe_inv : ⇑(equiv.inv G) = has_inv.inv := rfl
-
 @[simp, to_additive]
 lemma inv_symm : (equiv.inv G).symm = equiv.inv G := rfl
 
@@ -482,30 +470,22 @@ variables [group_with_zero G]
 
 /-- Left multiplication by a nonzero element in a `group_with_zero` is a permutation of the
 underlying type. -/
+@[simps {fully_applied := ff}]
 protected def mul_left' (a : G) (ha : a ≠ 0) : perm G :=
 { to_fun := λ x, a * x,
   inv_fun := λ x, a⁻¹ * x,
   left_inv := λ x, by { dsimp, rw [← mul_assoc, inv_mul_cancel ha, one_mul] },
   right_inv := λ x, by { dsimp, rw [← mul_assoc, mul_inv_cancel ha, one_mul] } }
 
-@[simp] lemma coe_mul_left' (a : G) (ha : a ≠ 0) : ⇑(equiv.mul_left' a ha) = (*) a := rfl
-
-@[simp] lemma mul_left'_symm_apply (a : G) (ha : a ≠ 0) :
-  ((equiv.mul_left' a ha).symm : G → G) = (*) a⁻¹ := rfl
-
 /-- Right multiplication by a nonzero element in a `group_with_zero` is a permutation of the
 underlying type. -/
+@[simps {fully_applied := ff}]
 protected def mul_right' (a : G) (ha : a ≠ 0) : perm G :=
 { to_fun := λ x, x * a,
   inv_fun := λ x, x * a⁻¹,
   left_inv := λ x, by { dsimp, rw [mul_assoc, mul_inv_cancel ha, mul_one] },
   right_inv := λ x, by { dsimp, rw [mul_assoc, inv_mul_cancel ha, mul_one] } }
 
-@[simp] lemma coe_mul_right' (a : G) (ha : a ≠ 0) : ⇑(equiv.mul_right' a ha) = λ x, x * a := rfl
-
-@[simp] lemma mul_right'_symm_apply (a : G) (ha : a ≠ 0) :
-  ((equiv.mul_right' a ha).symm : G → G) = λ x, x * a⁻¹ := rfl
-
 end group_with_zero
 
 end equiv

src/group_theory/free_abelian_group.lean

@@ -311,7 +311,8 @@ begin
 end
 
 lemma map_id : map id = add_monoid_hom.id (free_abelian_group α) :=
-eq.symm $ lift.ext _ _ $ λ x, lift.unique of (add_monoid_hom.id _) $ λ y, add_monoid_hom.id_apply _
+eq.symm $ lift.ext _ _ $ λ x, lift.unique of (add_monoid_hom.id _) $
+  λ y, add_monoid_hom.id_apply _ _
 
 lemma map_id_apply (x : free_abelian_group α) : map id x = x := by {rw map_id, refl }
 

src/group_theory/subgroup.lean

@@ -311,7 +311,7 @@ monoid_hom.mk' (λ x, ⟨x, h x.prop⟩) (λ ⟨a, ha⟩  ⟨b, hb⟩, rfl)
 
 @[simp, to_additive]
 lemma coe_inclusion {H K : subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a :=
-by { cases a, simp only [inclusion, coe_mk, monoid_hom.coe_mk'] }
+by { cases a, simp only [inclusion, coe_mk, monoid_hom.mk'_apply] }
 
 @[simp, to_additive]
 lemma subtype_comp_inclusion {H K : subgroup G} (hH : H ≤ K) :