chore(algebra/group/units): Make coercion the simp-normal form of uni…

…ts (#8568)

It's already used as the output for `@[simps]`; this makes `↑u` the simp-normal form of `u.val` and `↑(u⁻¹)` the simp-normal form of `u.inv`.

src/algebra/group/units.lean

@@ -108,10 +108,9 @@ by rw [←units.coe_one, eq_iff]
 
 @[simp, to_additive] lemma inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ := rfl
 
-@[to_additive] lemma val_coe : (↑a : α) = a.val := rfl
+@[simp, to_additive] lemma val_eq_coe : a.val = (↑a : α) := 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_eq_coe_inv : a.inv = ((a⁻¹ : units α) : α) := rfl
 
 @[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
 @[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _