feat: port Analysis.BoundedVariation (#4824)

This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Mathlib.lean

@@ -464,6 +464,7 @@ import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
 import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 import Mathlib.Analysis.Asymptotics.Theta
+import Mathlib.Analysis.BoundedVariation
 import Mathlib.Analysis.BoxIntegral.Basic
 import Mathlib.Analysis.BoxIntegral.Box.Basic
 import Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Mathlib/Algebra/Group/Basic.lean

@@ -1054,24 +1054,18 @@ lemma multiplicative_of_symmetric_of_isTotal
 
 /-- 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. -/
+  (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_isTotal "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."]
-lemma multiplicative_of_isTotal [Monoid β] (f : α → α → β) (r : α → α → Prop) [t : IsTotal α r]
-    (hswap : ∀ a b, f a b * f b a = 1)
-    (hmul : ∀ {a b c}, r a b → r b c → f a c = f a b * f b c)
-    (a b c : α) : f a c = f a b * f b c := by
-  have h : ∀ b c, r b c → f a c = f a b * f b c := by
-    intros b c hbc
-    obtain hab | hba := t.total a b
-    · exact hmul hab hbc
-    obtain hac | hca := t.total a c
-    · rw [hmul hba hac, ← mul_assoc, hswap a b, one_mul]
-    · rw [← one_mul (f a c), ← hswap a b, hmul hbc hca, mul_assoc, mul_assoc, hswap c a, mul_one]
-  obtain hbc | hcb := t.total b c
-  · exact h b c hbc
-  · rw [h c b hcb, mul_assoc, hswap c b, mul_one]
+`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`."]
+theorem multiplicative_of_isTotal (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 := by
+  apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
+  · simp_rw [and_imp]; exact @hswap
+  · exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
+  exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
 #align multiplicative_of_is_total multiplicative_of_isTotal
 #align additive_of_is_total additive_of_isTotal