α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (∏ᶠ (a : α) (b : β × γ), f (a, b)) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (∏ᶠ (abc : α × β × γ), f abc) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
rw [finprod_curry f h]
case e_f
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (fun a => ∏ᶠ (b : β × γ), f (a, b)) = fun a => ∏ᶠ (b : β) (c : γ), f (a, b, c)
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (∏ᶠ (a : α) (b : β × γ), f (a, b)) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
congr
case e_f.h
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ (∏ᶠ (b : β × γ), f (a, b)) = ∏ᶠ (b : β) (c : γ), f (a, b, c)
case e_f
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
⊢ (fun a => ∏ᶠ (b : β × γ), f (a, b)) = fun a => ∏ᶠ (b : β) (c : γ), f (a, b, c)
ext a
case e_f.h.hf
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ Set.Finite (mulSupport fun b => f (a, b))
case e_f.h
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ (∏ᶠ (b : β × γ), f (a, b)) = ∏ᶠ (b : β) (c : γ), f (a, b, c)
rw [finprod_curry]
no goals
case e_f.h.hf
α : Type u_2
β : Type u_3
ι : Type ?u.462199
G : Type ?u.462202
M : Type u_4
N : Type ?u.462208
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
γ : Type u_1
f : α × β × γ → M
h : Set.Finite (mulSupport f)
a : α
⊢ Set.Finite (mulSupport fun b => f (a, b))
simp [h]