α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i
have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f := by
  rw [mulSupport_comp_eq_preimage]
  exact (Equiv.plift.symm.image_eq_preimage _).symm
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i
have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
  rw [A, Finset.coe_map]
  exact image_subset _ h
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ i in Finset.map (Equiv.toEmbedding Equiv.plift.symm) s, f i.down = ∏ i in s, f i
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ (∏ᶠ (i : α), f i) = ∏ i in s, f i
rw [finprod_eq_prod_pLift_of_mulSupport_subset this]
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ x in s, f (↑Equiv.plift.symm x).down = ∏ i in s, f i
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ i in Finset.map (Equiv.toEmbedding Equiv.plift.symm) s, f i.down = ∏ i in s, f i
simp only [Finset.prod_map, Equiv.coe_toEmbedding]
no goals
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
⊢ ∏ x in s, f (↑Equiv.plift.symm x).down = ∏ i in s, f i
congr
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ PLift.down ⁻¹' mulSupport f = ↑Equiv.plift.symm '' mulSupport f
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
rw [mulSupport_comp_eq_preimage]
no goals
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ PLift.down ⁻¹' mulSupport f = ↑Equiv.plift.symm '' mulSupport f
exact (Equiv.plift.symm.image_eq_preimage _).symm
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ ↑Equiv.plift.symm '' mulSupport f ⊆ ↑(Equiv.toEmbedding Equiv.plift.symm) '' ↑s
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map (Equiv.toEmbedding Equiv.plift.symm) s)
rw [A, Finset.coe_map]
no goals
α : Type u_1
β : Type ?u.176909
ι : Type ?u.176912
G : Type ?u.176915
M : Type u_2
N : Type ?u.176921
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ↑Equiv.plift.symm '' mulSupport f
⊢ ↑Equiv.plift.symm '' mulSupport f ⊆ ↑(Equiv.toEmbedding Equiv.plift.symm) '' ↑s
exact image_subset _ h