feat(algebra/units): some norm_cast attributes (#2612)

Author: ChrisHughes24

src/algebra/group/units.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes
 -/
 import logic.function
 import algebra.group.to_additive
+import tactic.norm_cast
 
 /-!
 # Units (i.e., invertible elements) of a multiplicative monoid
@@ -66,10 +67,17 @@ ext.eq_iff.symm
   mul_left_inv := λ u, ext u.inv_val }
 
 variables (a b : units α) {c : units α}
-@[simp, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
-@[simp, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl
+@[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
+attribute [norm_cast] add_units.coe_add
+
+@[simp, norm_cast, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl
+attribute [norm_cast] add_units.coe_zero
+
 @[to_additive] lemma val_coe : (↑a : α) = a.val := rfl
-@[to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl
+
+@[norm_cast, to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl
+attribute [norm_cast] add_units.coe_neg
+
 @[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
 @[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _
 

src/algebra/group_power.lean

@@ -155,7 +155,7 @@ theorem is_add_monoid_hom.map_smul (f : A → B) [is_add_monoid_hom f] (a : A) (
   f (n • a) = n • f a :=
 (add_monoid_hom.of f).map_smul a n
 
-@[simp] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
+@[simp, norm_cast] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
 (units.coe_hom M).map_pow u n
 
 end monoid

src/group_theory/subgroup.lean

@@ -60,13 +60,14 @@ instance subtype.group {s : set G} [is_subgroup s] : group s :=
 instance subtype.comm_group {G : Type*} [comm_group G] {s : set G} [is_subgroup s] : comm_group s :=
 { .. subtype.group, .. subtype.comm_monoid }
 
-@[simp, to_additive]
+@[simp, norm_cast, to_additive]
 lemma is_subgroup.coe_inv {s : set G} [is_subgroup s] (a : s) : ((a⁻¹ : s) : G) = a⁻¹ := rfl
+attribute [norm_cast] is_add_subgroup.coe_neg
 
-@[simp] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : G) = a ^ n :=
+@[simp, norm_cast] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : G) = a ^ n :=
 by induction n; simp [is_submonoid.coe_pow a]
 
-@[simp] lemma is_add_subgroup.gsmul_coe {s : set A} [is_add_subgroup s] (a : s) (n : ℤ) :
+@[simp, norm_cast] lemma is_add_subgroup.gsmul_coe {s : set A} [is_add_subgroup s] (a : s) (n : ℤ) :
   ((gsmul n a : s) : A) = gsmul n a :=
 by induction n; simp [is_add_submonoid.smul_coe a]
 attribute [to_additive gsmul_coe] is_subgroup.coe_gpow

src/group_theory/submonoid.lean

@@ -237,20 +237,22 @@ instance subtype.comm_monoid {M} [comm_monoid M] {s : set M} [is_submonoid s] :
   .. subtype.monoid }
 
 /-- Submonoids inherit the 1 of the monoid. -/
-@[simp, to_additive "An `add_submonoid` inherits the 0 of the `add_monoid`. "]
+@[simp, norm_cast, to_additive "An `add_submonoid` inherits the 0 of the `add_monoid`. "]
 lemma is_submonoid.coe_one [is_submonoid s] : ((1 : s) : M) = 1 := rfl
+attribute [norm_cast] is_add_submonoid.coe_zero
 
 /-- Submonoids inherit the multiplication of the monoid. -/
-@[simp, to_additive "An `add_submonoid` inherits the addition of the `add_monoid`. "]
+@[simp, norm_cast, to_additive "An `add_submonoid` inherits the addition of the `add_monoid`. "]
 lemma is_submonoid.coe_mul [is_submonoid s] (a b : s) : ((a * b : s) : M) = a * b := rfl
+attribute [norm_cast] is_add_submonoid.coe_add
 
 /-- Submonoids inherit the exponentiation by naturals of the monoid. -/
-@[simp] lemma is_submonoid.coe_pow [is_submonoid s] (a : s) (n : ℕ) :
+@[simp, norm_cast] lemma is_submonoid.coe_pow [is_submonoid s] (a : s) (n : ℕ) :
   ((a ^ n : s) : M) = a ^ n :=
 by induction n; simp [*, pow_succ]
 
 /-- An `add_submonoid` inherits the multiplication by naturals of the `add_monoid`. -/
-@[simp] lemma is_add_submonoid.smul_coe {A : Type*} [add_monoid A] {s : set A}
+@[simp, norm_cast] lemma is_add_submonoid.smul_coe {A : Type*} [add_monoid A] {s : set A}
   [is_add_submonoid s] (a : s) (n : ℕ) : ((add_monoid.smul n a : s) : A) = add_monoid.smul n a :=
 by {induction n, refl, simp [*, succ_smul]}