no goals
α : Type u_2
β : Type u_1
ι : Type ?u.426329
G : Type ?u.426332
M : Type u_3
N : Type ?u.426338
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
classical
  rw [finprod_mem_finset_product']
  simp
α : Type u_2
β : Type u_1
ι : Type ?u.426329
G : Type ?u.426332
M : Type u_3
N : Type ?u.426338
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b)) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
α : Type u_2
β : Type u_1
ι : Type ?u.426329
G : Type ?u.426332
M : Type u_3
N : Type ?u.426338
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ (∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab) = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
rw [finprod_mem_finset_product']
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.426329
G : Type ?u.426332
M : Type u_3
N : Type ?u.426338
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset (α × β)
f : α × β → M
⊢ (∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.fst = a) s)), f (a, b)) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
simp