feat(algebra/group_with_zero): add eq_on_inv₀ (#16222)

* move some lemmas up in the import chain;
* use `namespace is_unit`;
* add `is_unit.eq_on_inv` and `eq_on_inv₀`;
* rename `monoid_hom.eq_on_inv` to `eq_on_inv`, make `f` and `g` explicit.

src/algebra/group/units.lean

@@ -221,6 +221,10 @@ by rw [←inv_mul_eq_one, inv_inv]
 @[to_additive] lemma inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
 units.inv_eq_of_mul_eq_one_right $ by rw [h, u₂.mul_inv]
 
+@[simp, to_additive]
+lemma coe_inv {M : Type*} [division_monoid M] (u : units M) : ↑u⁻¹ = (u⁻¹ : M) :=
+eq.symm $ inv_eq_of_mul_eq_one_right u.mul_inv
+
 end units
 
 /-- For `a, b` in a `comm_monoid` such that `a * b = 1`, makes a unit out of `a`. -/
@@ -420,66 +424,71 @@ 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
 
+namespace is_unit
+
 @[simp, to_additive]
-lemma is_unit.mul_iff [comm_monoid M] {x y : M} : is_unit (x * y) ↔ is_unit x ∧ is_unit y :=
+lemma 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⟩
 
+section monoid
+
+variables [monoid M] {a b c : M}
+
 /-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
 `α` is a `division_monoid`, use `is_unit.unit'` instead. -/
 @[to_additive "The element of the additive group of additive units, corresponding to an element of
 an additive monoid which is an additive unit. When `α` is a `subtraction_monoid`, use
 `is_add_unit.add_unit'` instead."]
-noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : Mˣ :=
+protected noncomputable def unit (h : is_unit a) : Mˣ :=
 (classical.some h).copy a (classical.some_spec h).symm _ rfl
 
 @[simp, to_additive]
-lemma is_unit.unit_of_coe_units [monoid M] {a : Mˣ} (h : is_unit (a : M)) : h.unit = a :=
+lemma unit_of_coe_units {a : Mˣ} (h : is_unit (a : M)) : h.unit = a :=
 units.ext $ rfl
 
-@[simp, to_additive]
-lemma is_unit.unit_spec [monoid M] {a : M} (h : is_unit a) : ↑h.unit = a :=
-rfl
+@[simp, to_additive] lemma unit_spec (h : is_unit a) : ↑h.unit = a := rfl
 
 @[simp, to_additive]
-lemma is_unit.coe_inv_mul [monoid M] {a : M} (h : is_unit a) :
-  ↑(h.unit)⁻¹ * a = 1 :=
-units.mul_inv _
+lemma coe_inv_mul (h : is_unit a) : ↑(h.unit)⁻¹ * a = 1 := units.mul_inv _
 
-@[simp, to_additive]
-lemma is_unit.mul_coe_inv [monoid M] {a : M} (h : is_unit a) :
-  a * ↑(h.unit)⁻¹ = 1 :=
-begin
-  convert units.mul_inv _,
-  simp [h.unit_spec]
-end
+@[simp, to_additive] lemma mul_coe_inv (h : is_unit a) : a * ↑(h.unit)⁻¹ = 1 :=
+by convert h.unit.mul_inv
 
 /-- `is_unit x` is decidable if we can decide if `x` comes from `Mˣ`. -/
-instance [monoid M] (x : M) [h : decidable (∃ u : Mˣ, ↑u = x)] : decidable (is_unit x) := h
+instance (x : M) [h : decidable (∃ u : Mˣ, ↑u = x)] : decidable (is_unit x) := h
 
-section monoid
-variables [monoid M] {a b c : M}
-
-@[to_additive] lemma is_unit.mul_left_inj (h : is_unit a) : b * a = c * a ↔ b = c :=
+@[to_additive] lemma mul_left_inj (h : is_unit a) : b * a = c * a ↔ b = c :=
 let ⟨u, hu⟩ := h in hu ▸ u.mul_left_inj
 
-@[to_additive] lemma is_unit.mul_right_inj (h : is_unit a) : a * b = a * c ↔ b = c :=
+@[to_additive] lemma mul_right_inj (h : is_unit a) : a * b = a * c ↔ b = c :=
 let ⟨u, hu⟩ := h in hu ▸ u.mul_right_inj
 
-@[to_additive] protected lemma is_unit.mul_left_cancel (h : is_unit a) : a * b = a * c → b = c :=
+@[to_additive] protected lemma mul_left_cancel (h : is_unit a) : a * b = a * c → b = c :=
 h.mul_right_inj.1
 
-@[to_additive] protected lemma is_unit.mul_right_cancel (h : is_unit b) : a * b = c * b → a = c :=
+@[to_additive] protected lemma mul_right_cancel (h : is_unit b) : a * b = c * b → a = c :=
 h.mul_left_inj.1
 
-@[to_additive] protected lemma is_unit.mul_right_injective (h : is_unit a) : injective ((*) a) :=
+@[to_additive] protected lemma mul_right_injective (h : is_unit a) : injective ((*) a) :=
 λ _ _, h.mul_left_cancel
 
-@[to_additive] protected lemma is_unit.mul_left_injective (h : is_unit b) : injective (* b) :=
+@[to_additive] protected lemma mul_left_injective (h : is_unit b) : injective (* b) :=
 λ _ _, h.mul_right_cancel
 
 end monoid
-end is_unit
+
+variables [division_monoid M] {a : M}
+
+@[simp, to_additive] protected lemma inv_mul_cancel : is_unit a → a⁻¹ * a = 1 :=
+by { rintro ⟨u, rfl⟩, rw [← units.coe_inv, units.inv_mul] }
+
+@[simp, to_additive] protected lemma mul_inv_cancel : is_unit a → a * a⁻¹ = 1 :=
+by { rintro ⟨u, rfl⟩, rw [← units.coe_inv, units.mul_inv] }
+
+end is_unit -- namespace
+
+end is_unit -- section
 
 section noncomputable_defs
 

src/algebra/group_with_zero/basic.lean

@@ -39,7 +39,7 @@ set_option old_structure_cmd true
 open_locale classical
 open function
 
-variables {α M₀ G₀ M₀' G₀' F : Type*}
+variables {α M₀ G₀ M₀' G₀' F F' : Type*}
 
 section
 
@@ -976,14 +976,25 @@ end commute
 
 section monoid_with_zero
 variables [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀]
-  [monoid_with_zero_hom_class F G₀ M₀] (f : F) {a : G₀}
+  [monoid_with_zero M₀'] [monoid_with_zero_hom_class F G₀ M₀]
+  [monoid_with_zero_hom_class F' G₀ M₀'] (f : F) {a : G₀}
 include M₀
 
 lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
 ⟨λ hfa ha, hfa $ ha.symm ▸ map_zero f, λ ha, ((is_unit.mk0 a ha).map f).ne_zero⟩
 
 @[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 := not_iff_not.1 (map_ne_zero f)
 
+omit M₀
+include M₀'
+
+lemma eq_on_inv₀ (f g : F') (h : f a = g a) : f a⁻¹ = g a⁻¹ :=
+begin
+  rcases eq_or_ne a 0 with rfl|ha,
+  { rw [inv_zero, map_zero, map_zero] },
+  { exact (is_unit.mk0 a ha).eq_on_inv f g h }
+end
+
 end monoid_with_zero
 
 section group_with_zero

src/algebra/hom/equiv.lean

@@ -503,9 +503,6 @@ def to_units [group G] : G ≃* Gˣ :=
 @[simp, to_additive] lemma coe_to_units [group G] (g : G) :
   (to_units g : G) = g := rfl
 
-@[to_additive]
-protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := (to_units x).is_unit
-
 namespace units
 
 variables [monoid M] [monoid N] [monoid P]

src/algebra/hom/group.lean

@@ -356,6 +356,9 @@ attribute [to_additive_reorder 8, to_additive] map_zpow
 
 end mul_one
 
+@[to_additive] lemma group.is_unit [group G] (g : G) : is_unit g :=
+⟨⟨g, g⁻¹, mul_inv_self g, inv_mul_self g⟩, rfl⟩
+
 section mul_zero_one
 
 variables [mul_zero_one_class M] [mul_zero_one_class N]
@@ -1061,13 +1064,21 @@ by { ext, simp only [map_one, coe_comp, function.comp_app, one_apply] }
   g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ :=
 by { ext, simp only [mul_apply, function.comp_app, map_mul, coe_comp] }
 
+/-- If two homomorphisms from a division monoid to a monoid are equal at a unit `x`, then they are
+equal at `x⁻¹`. -/
+@[to_additive "If two homomorphisms from a subtraction monoid to an additive monoid are equal at an
+additive unit `x`, then they are equal at `-x`."]
+lemma _root_.is_unit.eq_on_inv {G N} [division_monoid G] [monoid N] [monoid_hom_class F G N] {x : G}
+  (hx : is_unit x) (f g : F) (h : f x = g x) : f x⁻¹ = g x⁻¹ :=
+left_inv_eq_right_inv (map_mul_eq_one f hx.inv_mul_cancel) $
+  h.symm ▸ map_mul_eq_one g $ hx.mul_inv_cancel
+
 /-- If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`. -/
 @[to_additive "If two homomorphism from an additive group to an additive monoid are equal at `x`,
 then they are equal at `-x`." ]
-lemma eq_on_inv {G} [group G] [monoid M] [monoid_hom_class F G M] {f g : F} {x : G}
+lemma _root_.eq_on_inv {G} [group G] [monoid M] [monoid_hom_class F G M] (f g : F) {x : G}
   (h : f x = g x) : f x⁻¹ = g x⁻¹ :=
-left_inv_eq_right_inv (map_mul_eq_one f $ inv_mul_self x) $
-  h.symm ▸ map_mul_eq_one g $ mul_inv_self x
+(group.is_unit x).eq_on_inv f g h
 
 /-- Group homomorphisms preserve inverse. -/
 @[to_additive "Additive group homomorphisms preserve negation."]

src/algebra/hom/units.lean

@@ -67,9 +67,6 @@ lemma coe_pow (u : Mˣ) (n : ℕ) : ((u ^ n : Mˣ) : M) = u ^ n :=
 section division_monoid
 variables [division_monoid α]
 
-@[simp, norm_cast, to_additive] lemma coe_inv : ∀ u : αˣ, ↑u⁻¹ = (u⁻¹ : α) :=
-(units.coe_hom α).map_inv
-
 @[simp, norm_cast, to_additive] lemma coe_div : ∀ u₁ u₂ : αˣ, ↑(u₁ / u₂) = (u₁ / u₂ : α) :=
 (units.coe_hom α).map_div
 
@@ -118,12 +115,9 @@ and `f.to_hom_units` is the corresponding monoid homomorphism from `G` to `Mˣ`.
 then its image lies in the `add_units` of `M`,
 and `f.to_hom_units` is the corresponding homomorphism from `G` to `add_units M`."]
 def to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) : G →* Mˣ :=
-{ to_fun := λ g,
-    ⟨f g, f (g⁻¹),
-      by rw [← f.map_mul, mul_inv_self, f.map_one],
-      by rw [← f.map_mul, inv_mul_self, f.map_one]⟩,
-  map_one' := units.ext (f.map_one),
-  map_mul' := λ _ _, units.ext (f.map_mul _ _) }
+units.lift_right f
+  (λ g, ⟨f g, f g⁻¹, map_mul_eq_one f (mul_inv_self _), map_mul_eq_one f (inv_mul_self _)⟩)
+  (λ g, rfl)
 
 @[simp] lemma coe_to_hom_units {G M : Type*} [group G] [monoid M] (f : G →* M) (g : G):
   (f.to_hom_units g : M) = f g := rfl
@@ -162,12 +156,6 @@ end monoid
 section division_monoid
 variables [division_monoid α] {a b c : α}
 
-@[simp, to_additive] protected lemma inv_mul_cancel : is_unit a → a⁻¹ * a = 1 :=
-by { rintro ⟨u, rfl⟩, rw [←units.coe_inv, units.inv_mul] }
-
-@[simp, to_additive] protected lemma mul_inv_cancel : is_unit a → a * a⁻¹ = 1 :=
-by { rintro ⟨u, rfl⟩, rw [←units.coe_inv, units.mul_inv] }
-
 /-- The element of the group of units, corresponding to an element of a monoid which is a unit. As
 opposed to `is_unit.unit`, the inverse is computable and comes from the inversion on `α`. This is
 useful to transfer properties of inversion in `units α` to `α`. See also `to_units`. -/

src/data/int/cast.lean

@@ -177,7 +177,7 @@ if `f 1 = g 1`. -/
 @[ext] theorem ext_int [add_monoid A] {f g : ℤ →+ A} (h1 : f 1 = g 1) : f = g :=
 have f.comp (int.of_nat_hom : ℕ →+ ℤ) = g.comp (int.of_nat_hom : ℕ →+ ℤ) := ext_nat' _ _ h1,
 have ∀ n : ℕ, f n = g n := ext_iff.1 this,
-ext $ λ n, int.cases_on n this $ λ n, eq_on_neg (this $ n + 1)
+ext $ λ n, int.cases_on n this $ λ n, eq_on_neg _ _ (this $ n + 1)
 
 variables [add_group_with_one A]