feat(algebra/group/basic): reduce additivity checks to one case (#18080)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/group/basic.lean

@@ -651,3 +651,47 @@ lemma bit1_sub [has_one M] (a b : M) : bit1 (a - b) = bit1 a - bit0 b :=
 (congr_arg (+ (1 : M)) $ bit0_sub a b : _).trans $ sub_add_eq_add_sub _ _ _
 
 end subtraction_comm_monoid
+
+section multiplicative
+
+variables [monoid β] (p r : α → α → Prop) [is_total α r] (f : α → α → β)
+
+@[to_additive additive_of_symmetric_of_is_total]
+lemma multiplicative_of_symmetric_of_is_total
+  (hsymm : symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1)
+  (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c)
+  {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c :=
+begin
+  suffices : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c,
+  { obtain rbc | rcb := total_of r b c,
+    { exact this rbc pab pbc pac },
+    { rw [this rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one] } },
+  intros b c rbc pab pbc pac,
+  obtain rab | rba := total_of r a b,
+  { exact hmul rab rbc pab pbc pac },
+  rw [← one_mul (f a c), ← hf_swap pab, mul_assoc],
+  obtain rac | rca := total_of r a c,
+  { rw [hmul rba rac (hsymm pab) pac pbc] },
+  { rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one] },
+end
+
+/-- If a binary function from a type equipped with a total relation `r` to a monoid is
+  anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
+  (i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
+  We allow restricting to a subset specified by a predicate `p`. -/
+@[to_additive additive_of_is_total "If a binary function from a type equipped with a total relation
+  `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in order to show
+  it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and `r b c`
+  are satisfied. We allow restricting to a subset specified by a predicate `p`."]
+lemma multiplicative_of_is_total (p : α → Prop)
+  (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
+  (hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c)
+  {a b c : α} (pa : p a) (pb : p b) (pc : p c) : f a c = f a b * f b c :=
+begin
+  apply multiplicative_of_symmetric_of_is_total (λ a b, p a ∧ p b) r f (λ _ _, and.swap),
+  { simp_rw and_imp, exact @hswap },
+  { exact λ a b c rab rbc pab pbc pac, hmul rab rbc pab.1 pab.2 pac.2 },
+  exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩],
+end
+
+end multiplicative