G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i in Finite.toFinset ?hc, f i.down = ∏ i in s, f i.down

case hc
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i.down
rw [finprod, dif_pos]
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : ¬x ∈ Finite.toFinset hf
⊢ f x.down = 1
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i in Finite.toFinset ?hc, f i.down = ∏ i in s, f i.down

case hc
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
refine' Finset.prod_subset hs fun x _ hxf => _
no goals
G : Type ?u.27905
M : Type u_2
N : Type ?u.27911
α : Sort u_1
β : Sort ?u.27917
ι : Sort ?u.27920
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport (f ∘ PLift.down))
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : ¬x ∈ Finite.toFinset hf
⊢ f x.down = 1
rwa [hf.mem_toFinset, nmem_mulSupport] at hxf