feat: (∏ᶠ i, f i) a = ∏ᶠ i, f i a (#20203)

From FLT

Co-authored-by: Kevin Buzzard

Author: YaelDillies

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying, Kevin Buzzard, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
+import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.Group.FiniteSupport
 import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
@@ -319,13 +320,17 @@ theorem finprod_eq_mulIndicator_apply (s : Set α) (f : α → M) (a : α) :
   classical convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)
 
 @[to_additive (attr := simp)]
-theorem finprod_mem_mulSupport (f : α → M) (a : α) : ∏ᶠ _ : f a ≠ 1, f a = f a := by
+theorem finprod_apply_ne_one (f : α → M) (a : α) : ∏ᶠ _ : f a ≠ 1, f a = f a := by
   rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]
 
 @[to_additive]
 theorem finprod_mem_def (s : Set α) (f : α → M) : ∏ᶠ a ∈ s, f a = ∏ᶠ a, mulIndicator s f a :=
   finprod_congr <| finprod_eq_mulIndicator_apply s f
 
+@[to_additive]
+lemma finprod_mem_mulSupport (f : α → M) : ∏ᶠ a ∈ mulSupport f, f a = ∏ᶠ a, f a := by
+  rw [finprod_mem_def, mulIndicator_mulSupport]
+
 @[to_additive]
 theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h : mulSupport f ⊆ s) :
     ∏ᶠ i, f i = ∏ i ∈ s, f i := by
@@ -921,6 +926,16 @@ theorem finprod_mem_sUnion {t : Set (Set α)} (h : t.PairwiseDisjoint id) (ht₀
   rw [Set.sUnion_eq_biUnion]
   exact finprod_mem_biUnion h ht₀ ht₁
 
+@[to_additive]
+lemma finprod_option {f : Option α → M} (hf : (mulSupport (f ∘ some)).Finite) :
+    ∏ᶠ o, f o = f none * ∏ᶠ a, f (some a) := by
+  replace hf : (mulSupport f).Finite := by simpa [finite_option]
+  convert finprod_mem_insert' f (show none ∉ Set.range Option.some by aesop)
+    (hf.subset inter_subset_right)
+  · aesop
+  · rw [finprod_mem_range]
+    exact Option.some_injective _
+
 @[to_additive]
 theorem mul_finprod_cond_ne (a : α) (hf : (mulSupport f).Finite) :
     (f a * ∏ᶠ (i) (_ : i ≠ a), f i) = ∏ᶠ i, f i := by
@@ -1008,6 +1023,15 @@ theorem finsum_mul {R : Type*} [Semiring R] (f : α → R) (r : R) (h : (support
     (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
   (AddMonoidHom.mulRight r).map_finsum h
 
+@[to_additive (attr := simp)]
+lemma finprod_apply {α ι : Type*} {f : ι → α → N} (hf : (mulSupport f).Finite) (a : α) :
+    (∏ᶠ i, f i) a = ∏ᶠ i, f i a := by
+  classical
+  have hf' : (mulSupport fun i ↦ f i a).Finite := hf.subset (by aesop)
+  simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
+  symm
+  apply Finset.prod_subset <;> aesop
+
 @[to_additive]
 theorem Finset.mulSupport_of_fiberwise_prod_subset_image [DecidableEq β] (s : Finset α) (f : α → M)
     (g : α → β) : (mulSupport fun b => (s.filter fun a => g a = b).prod f) ⊆ s.image g := by