feat(algebra/big_operators/finprod): add lemma `finprod_mem_finset_of…

…_product` (#7439)

src/algebra/big_operators/finprod.lean

@@ -204,6 +204,10 @@ open_locale big_operators
   ∏ᶠ (h : a ∈ s), f a = mul_indicator s f a :=
 by convert finprod_eq_if
 
+@[simp, to_additive] lemma finprod_mem_mul_support (f : α → M) (a : α) :
+  ∏ᶠ (h : f a ≠ 1), f a = f a :=
+by rw [← mem_mul_support, finprod_eq_mul_indicator_apply, mul_indicator_mul_support]
+
 @[to_additive] lemma finprod_mem_def (s : set α) (f : α → M) :
   ∏ᶠ a ∈ s, f a = ∏ᶠ a, mul_indicator s f a :=
 finprod_congr $ finprod_eq_mul_indicator_apply s f
@@ -699,6 +703,58 @@ lemma finsum_mul {R : Type*} [semiring R] (f : α → R) (r : R)
   (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
 (add_monoid_hom.mul_right r).map_finsum h
 
+@[to_additive] lemma finset.mul_support_of_fiberwise_prod_subset_image [decidable_eq β]
+  (s : finset α) (f : α → M) (g : α → β) :
+  mul_support (λ b, (s.filter (λ a, g a = b)).prod f) ⊆ s.image g :=
+begin
+  simp only [finset.coe_image, set.mem_image, finset.mem_coe, function.support_subset_iff],
+  intros b h,
+  suffices : (s.filter (λ (a : α), g a = b)).nonempty,
+  { simpa only [s.fiber_nonempty_iff_mem_image g b, finset.mem_image, exists_prop], },
+  exact finset.nonempty_of_prod_ne_one h,
+end
+
+/-- Note that `b ∈ (s.filter (λ ab, prod.fst ab = a)).image prod.snd` iff `(a, b) ∈ s` so we can
+simplify the right hand side of this lemma. However the form stated here is more useful for
+iterating this lemma, e.g., if we have `f : α × β × γ → M`. -/
+@[to_additive] lemma finprod_mem_finset_product' [decidable_eq α] [decidable_eq β]
+  (s : finset (α × β)) (f : α × β → M) :
+  ∏ᶠ ab (h : ab ∈ s), f ab =
+  ∏ᶠ a b (h : b ∈ (s.filter (λ ab, prod.fst ab = a)).image prod.snd), f (a, b) :=
+begin
+  have : ∀ a, ∏ (i : β) in (s.filter (λ ab, prod.fst ab = a)).image prod.snd, f (a, i) =
+    (finset.filter (λ ab, prod.fst ab = a) s).prod f,
+  { intros a, apply finset.prod_bij (λ b _, (a, b)); finish, },
+  rw finprod_mem_finset_eq_prod,
+  simp_rw [finprod_mem_finset_eq_prod, this],
+  rw [finprod_eq_prod_of_mul_support_subset _
+    (s.mul_support_of_fiberwise_prod_subset_image f prod.fst),
+    ← finset.prod_fiberwise_of_maps_to _ f],
+  finish,
+end
+
+/-- See also `finprod_mem_finset_product'`. -/
+@[to_additive] lemma finprod_mem_finset_product (s : finset (α × β)) (f : α × β → M) :
+  ∏ᶠ ab (h : ab ∈ s), f ab = ∏ᶠ a b (h : (a, b) ∈ s), f (a, b) :=
+by { classical, rw finprod_mem_finset_product', simp, }
+
+@[to_additive] lemma finprod_mem_finset_product₃ {γ : Type*}
+  (s : finset (α × β × γ)) (f : α × β × γ → M) :
+  ∏ᶠ abc (h : abc ∈ s), f abc = ∏ᶠ a b c (h : (a, b, c) ∈ s), f (a, b, c) :=
+by { classical, rw finprod_mem_finset_product', simp_rw finprod_mem_finset_product', simp, }
+
+@[to_additive] lemma finprod_curry (f : α × β → M) (hf : (mul_support f).finite) :
+  ∏ᶠ ab, f ab = ∏ᶠ a b, f (a, b) :=
+begin
+  have h₁ : ∀ a, ∏ᶠ (h : a ∈ hf.to_finset), f a = f a, { simp, },
+  have h₂ : ∏ᶠ a, f a = ∏ᶠ a (h : a ∈ hf.to_finset), f a, { simp, },
+  simp_rw [h₂, finprod_mem_finset_product, h₁],
+end
+
+@[to_additive] lemma finprod_curry₃ {γ : Type*} (f : α × β × γ → M) (h : (mul_support f).finite) :
+  ∏ᶠ abc, f abc = ∏ᶠ a b c, f (a, b, c) :=
+by { rw finprod_curry f h, congr, ext a, rw finprod_curry, simp [h], }
+
 @[to_additive]
 lemma finprod_dmem {s : set α} [decidable_pred (∈ s)] (f : (Π (a : α), a ∈ s → M)) :
   ∏ᶠ (a : α) (h : a ∈ s), f a h = ∏ᶠ (a : α) (h : a ∈ s), if h' : a ∈ s then f a h' else 1 :=

src/data/support.lean

@@ -127,6 +127,15 @@ set.ext $ λ x, by simp only [mul_support, not_and_distrib, mem_union_eq, mem_se
   mul_support f = mul_support (λ x, (f x).1) ∪ mul_support (λ x, (f x).2) :=
 by simp only [← mul_support_prod_mk, prod.mk.eta]
 
+@[to_additive] lemma mul_support_along_fiber_subset (f : α × β → M) (a : α) :
+  mul_support (λ b, f (a, b)) ⊆ (mul_support f).image prod.snd :=
+by tidy
+
+@[simp, to_additive] lemma mul_support_along_fiber_finite_of_finite
+  (f : α × β → M) (a : α) (h : (mul_support f).finite) :
+  (mul_support (λ b, f (a, b))).finite :=
+(h.image prod.snd).subset (mul_support_along_fiber_subset f a)
+
 end has_one
 
 @[to_additive] lemma mul_support_mul [monoid M] (f g : α → M) :