refactor(algebra/group/defs): inv_one_class, neg_zero_class (#16187)

Define typeclasses `inv_one_class` and `neg_zero_class`, to allow
results depending on those properties to be proved more generally than
for `division_monoid` and `subtraction_monoid` without requiring
duplication.  Also define `div_inv_one_monoid` and `sub_neg_zero_monoid`.

The only instances added here are those deduced from `division_monoid`
and `subtraction_monoid`, and the only lemmas generalized to these
classes were previously proved for those classes.  Additional
instances intended for followups include:

* `neg_zero_class` for the combination of `mul_zero_class` with
  `has_distrib_neg`, so eliminating the separate `neg_zero'` lemma.

* `sub_neg_zero_monoid` for `ereal`.

* `div_inv_one_monoid` for `ennreal`.

* The usual `pointwise`, `pi` and `prod` instances.

Additional lemmas intended to be generalized to use these typeclasses
in followups include:

* `antiperiodic.nat_mul_eq_of_eq_zero` and
  `antiperiodic.int_mul_eq_of_eq_zero`, which currently require the
  codomain of the antiperiodic function to be a `subtraction_monoid`.
  (The latter will also require involutive `neg`, as will some lemmas
  about inequalities.)

* Given appropriate typeclasses for the interaction of inequalities
  with `inv` and `neg` (which will also enabling combining `left` and
  `right` variants, which is the main motivation of these changes),
  lemmas such as `left.inv_le_one_iff`, `left.one_le_inv_iff`,
  `left.one_lt_inv_iff`, `left.inv_lt_one_iff` and their `right` and
  additive variants.  Some of these currently have duplicates for
  `ennreal`, for example.

  Zulip thread raising question of such typeclasses:
  https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclasses.20for.20orders.20with.20neg.20and.20inv

src/algebra/group/basic.lean

@@ -244,6 +244,17 @@ by rw [div_eq_mul_inv, one_div]
 
 end div_inv_monoid
 
+section div_inv_one_monoid
+variables [div_inv_one_monoid G]
+
+@[simp, to_additive] lemma div_one (a : G) : a / 1 = a :=
+by simp [div_eq_mul_inv]
+
+@[to_additive] lemma one_div_one : (1 : G) / 1 = 1 :=
+div_one _
+
+end div_inv_one_monoid
+
 section division_monoid
 variables [division_monoid α] {a b c : α}
 
@@ -275,12 +286,13 @@ variables (a b c)
 @[to_additive] lemma inv_div_left : a⁻¹ / b = (b * a)⁻¹ := by simp
 @[simp, to_additive] lemma inv_div : (a / b)⁻¹ = b / a := by simp
 @[simp, to_additive] lemma one_div_div : 1 / (a / b) = b / a := by simp
-@[simp, to_additive] lemma inv_one : (1 : α)⁻¹ = 1 :=
-by simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm
-@[simp, to_additive] lemma div_one : a / 1 = a := by simp
-@[to_additive] lemma one_div_one : (1 : α) / 1 = 1 := div_one _
 @[to_additive] lemma one_div_one_div : 1 / (1 / a) = a := by simp
 
+@[priority 100, to_additive] instance division_monoid.to_div_inv_one_monoid :
+  div_inv_one_monoid α :=
+{ inv_one := by simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm,
+  ..division_monoid.to_div_inv_monoid α }
+
 variables {a b c}
 
 @[simp, to_additive] lemma inv_eq_one : a⁻¹ = 1 ↔ a = 1 := inv_injective.eq_iff' inv_one

src/algebra/group/defs.lean

@@ -659,6 +659,38 @@ alias div_eq_mul_inv ← division_def
 
 end div_inv_monoid
 
+section inv_one_class
+
+set_option extends_priority 50
+
+/-- Typeclass for expressing that `-0 = 0`. -/
+class neg_zero_class (G : Type*) extends has_zero G, has_neg G :=
+(neg_zero : -(0 : G) = 0)
+
+/-- A `sub_neg_monoid` where `-0 = 0`. -/
+class sub_neg_zero_monoid (G : Type*) extends sub_neg_monoid G, neg_zero_class G
+
+/-- Typeclass for expressing that `1⁻¹ = 1`. -/
+@[to_additive]
+class inv_one_class (G : Type*) extends has_one G, has_inv G :=
+(inv_one : (1 : G)⁻¹ = 1)
+
+attribute [to_additive neg_zero_class.to_has_neg] inv_one_class.to_has_inv
+attribute [to_additive neg_zero_class.to_has_zero] inv_one_class.to_has_one
+
+/-- A `div_inv_monoid` where `1⁻¹ = 1`. -/
+@[to_additive sub_neg_zero_monoid]
+class div_inv_one_monoid (G : Type*) extends div_inv_monoid G, inv_one_class G
+
+attribute [to_additive sub_neg_zero_monoid.to_sub_neg_monoid] div_inv_one_monoid.to_div_inv_monoid
+attribute [to_additive sub_neg_zero_monoid.to_neg_zero_class] div_inv_one_monoid.to_inv_one_class
+
+variables [inv_one_class G]
+
+@[simp, to_additive] lemma inv_one : (1 : G)⁻¹ = 1 := inv_one_class.inv_one
+
+end inv_one_class
+
 /-- A `subtraction_monoid` is a `sub_neg_monoid` with involutive negation and such that
 `-(a + b) = -b + -a` and `a + b = 0 → -a = b`. -/
 @[protect_proj, ancestor sub_neg_monoid has_involutive_neg]

src/tactic/abel.lean

@@ -181,7 +181,7 @@ by simp [h₂.symm, h₁.symm, termg]; ac_refl
 
 meta def eval_neg (c : context) : normal_expr → tactic (normal_expr × expr)
 | (zero e) := do
-  p ← c.mk_app ``neg_zero ``subtraction_monoid [],
+  p ← c.mk_app ``neg_zero ``neg_zero_class [],
   return (zero' c, p)
 | (nterm e n x a) := do
   (n', h₁) ← mk_app ``has_neg.neg [n.1] >>= norm_num.eval_field,