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