feat(data/equiv/mul_add): add units.coe_inv (#8477)

* rename old `units.coe_inv` to `units.coe_inv''`;
* add new `@[simp, norm_cast, to_additive] lemma units.coe_inv` about
  coercion of units of a group;
* add missing `coe_to_units`.

src/algebra/group/units.lean

@@ -110,8 +110,8 @@ by rw [←units.coe_one, eq_iff]
 
 @[to_additive] lemma val_coe : (↑a : α) = a.val := rfl
 
-@[norm_cast, to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl
-attribute [norm_cast] add_units.coe_neg
+@[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 _
@@ -165,7 +165,7 @@ calc ↑u⁻¹ = ↑u⁻¹ * 1 : by rw mul_one
       ... = a : by rw [u.inv_mul, one_mul]
 
 lemma inv_unique {u₁ u₂ : units α} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
-suffices ↑u₁ * (↑u₂⁻¹ : α) = 1, by exact inv_eq_of_mul_eq_one this, by rw [h, u₂.mul_inv]
+inv_eq_of_mul_eq_one $ by rw [h, u₂.mul_inv]
 
 end units
 

src/data/equiv/mul_add.lean

@@ -405,17 +405,24 @@ h.to_add_monoid_hom.map_sub x y
 
 /-- 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 :=
+def to_units [group G] : G ≃* units G :=
 { to_fun := λ x, ⟨x, x⁻¹, mul_inv_self _, inv_mul_self _⟩,
   inv_fun := coe,
   left_inv := λ x, rfl,
   right_inv := λ u, units.ext rfl,
   map_mul' := λ x y, units.ext rfl }
 
+@[simp, to_additive coe_to_add_units] lemma coe_to_units [group G] (g : G) :
+  (to_units g : G) = g := rfl
+
 protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := (to_units x).is_unit
 
 namespace units
 
+@[simp, to_additive] lemma coe_inv [group G] (u : units G) :
+  ↑u⁻¹ = (u⁻¹ : G) :=
+to_units.symm.map_inv u
+
 variables [monoid M] [monoid N] [monoid P]
 
 /-- A multiplicative equivalence of monoids defines a multiplicative equivalence