English
If p is a predicate on α and IsTotal α r, and f follows a symmetric/anti-symmetric pattern with p, then f is multiplicative on p-triples: f a c = f a b · f b c whenever pa, pb, pc hold.
Русский
Если p — предикат на α и IsTotal α r, и f удовлетворяет симметричному/антисимметричному шаблону, тогда f является умножаемой на тройках, удовлетворяющих p: f a c = f a b · f b c при pa, pb, pc.
LaTeX
$$(hsymm : Symmetric p) → (hf_swap : ∀ {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}, p a → p b → p c → f a c = f a b * f b c$$
Lean4
@[to_additive additive_of_symmetric_of_isTotal]
theorem multiplicative_of_symmetric_of_isTotal (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 :=
by
have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c :=
by
intro 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]
obtain rbc | rcb := total_of r b c
· exact hmul' rbc pab pbc pac
· rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
