feat(algebra/group/units): generalize units.coe_lift (#11057)

* Generalize `units.coe_lift` from `group_with_zero` to `monoid`; use condition `is_unit` instead of `≠ 0`.
* Add some missing `@[to_additive]` attrs.

src/algebra/group/units.lean

@@ -261,10 +261,18 @@ a two-sided additive inverse. The actual definition says that `a` is equal to so
 `u : add_units M`, where `add_units M` is a bundled version of `is_add_unit`."]
 def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, (u : M) = a
 
-@[nontriviality] lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
+@[nontriviality, to_additive is_add_unit_of_subsingleton]
+lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
 ⟨⟨a, a, subsingleton.elim _ _, subsingleton.elim _ _⟩, rfl⟩
 
-instance [monoid M] [subsingleton M] : unique (units M) :=
+attribute [nontriviality] is_add_unit_of_subsingleton
+
+@[to_additive] instance [monoid M] : can_lift M (units M) :=
+{ coe := coe,
+  cond := is_unit,
+  prf := λ _, id }
+
+@[to_additive] instance [monoid M] [subsingleton M] : unique (units M) :=
 { default := 1,
   uniq := λ a, units.coe_eq_one.mp $ subsingleton.elim (a : M) 1 }
 
@@ -331,7 +339,7 @@ is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
   (hu : is_unit (x * y)) : is_unit y :=
 @is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
 
-@[simp]
+@[simp, to_additive]
 lemma is_unit.mul_iff [comm_monoid M] {x y : M} : is_unit (x * y) ↔ is_unit x ∧ is_unit y :=
 ⟨λ h, ⟨is_unit_of_mul_is_unit_left h, is_unit_of_mul_is_unit_right h⟩,
   λ h, is_unit.mul h.1 h.2⟩
@@ -379,7 +387,7 @@ noncomputable def group_of_is_unit [hM : monoid M] (h : ∀ (a : M), is_unit a)
   mul_left_inv := λ a, by
   { change ↑((h a).unit)⁻¹ * a = 1,
     rw [units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one] },
-.. hM }
+  .. hM }
 
 /-- Constructs a `comm_group` structure on a `comm_monoid` consisting only of units. -/
 noncomputable def comm_group_of_is_unit [hM : comm_monoid M] (h : ∀ (a : M), is_unit a) :
@@ -388,6 +396,6 @@ noncomputable def comm_group_of_is_unit [hM : comm_monoid M] (h : ∀ (a : M), i
   mul_left_inv := λ a, by
   { change ↑((h a).unit)⁻¹ * a = 1,
     rw [units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one] },
-.. hM }
+  .. hM }
 
 end noncomputable_defs

src/algebra/group_with_zero/basic.lean

@@ -719,11 +719,6 @@ begin
     simpa only [eq_comm] using units.exists_iff_ne_zero.mpr h }
 end
 
-instance : can_lift G₀ (units G₀) :=
-{ coe := coe,
-  cond := (≠ 0),
-  prf := λ x, exists_iff_ne_zero.mpr }
-
 end units
 
 section group_with_zero

src/group_theory/submonoid/center.lean

@@ -86,7 +86,7 @@ lemma inv_mem_center₀ [group_with_zero M] {a : M} (ha : a ∈ set.center M) :
 begin
   obtain rfl | ha0 := eq_or_ne a 0,
   { rw inv_zero, exact zero_mem_center M },
-  lift a to units M using ha0,
+  rcases is_unit.mk0 _ ha0 with ⟨a, rfl⟩,
   rw ←units.coe_inv',
   exact center_units_subset (inv_mem_center (subset_center_units ha)),
 end