Source indexedlemma · leanprover/lean4:v4.32.0

Finset.prod_finset_product_filter_right

Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:734 to 744

Mathematical statement

Exact Lean statement

@[to_additive]
lemma Finset.prod_finset_product_filter_right {α β γ : Type*} {s : Finset α} {t : Finset β}
    {p : α → Prop} {q : α → β → Prop} [DecidablePred p] [DecidableRel q]
    [DecidablePred fun r : α × β ↦ p r.1 ∧ q r.1 r.2] {f : α → β → γ} [CommMonoid γ] :
    ∏ x ∈ s with p x, ∏ y ∈ t with q x y, f x y =
    ∏ r ∈ s ×ˢ t with p r.1 ∧ q r.1 r.2, f r.1 r.2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[to_additive]lemma Finset.prod_finset_product_filter_right {α β γ : Type*} {s : Finset α} {t : Finset β}    {p : α → Prop} {q : α → β → Prop} [DecidablePred p] [DecidableRel q]    [DecidablePred fun r : α × β ↦ p r.1 ∧ q r.1 r.2] {f : α → β → γ} [CommMonoid γ] :    ∏ x ∈ s with p x, ∏ y ∈ t with q x y, f x y =    ∏ r ∈ s ×ˢ t with p r.1 ∧ q r.1 r.2, f r.1 r.2 := by  convert (prod_finset_product_right' ((t ×ˢ s).filter fun r ↦ p r.2 ∧ q r.2 r.1) _ _ _).symm  · refine Finset.prod_equiv (Equiv.prodComm α β) (fun r ↦ ?_) (by simp)    simp_rw [mem_filter, mem_product, Equiv.prodComm_apply, Prod.fst_swap, Prod.snd_swap]    tauto  · intro r; simp only [mem_filter, mem_product]; tauto