G : Type ?u.29447
M : Type u_2
N : Type ?u.29453
α : Sort u_1
β : Sort ?u.29459
ι : Sort ?u.29462
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
G : Type ?u.29447
M : Type u_2
N : Type ?u.29453
α : Sort u_1
β : Sort ?u.29459
ι : Sort ?u.29462
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ Finite.toFinset (_ : Set.Finite (mulSupport (f ∘ PLift.down)))
⊢ x ∈ s
rw [Finite.mem_toFinset] at hx
no goals
G : Type ?u.29447
M : Type u_2
N : Type ?u.29453
α : Sort u_1
β : Sort ?u.29459
ι : Sort ?u.29462
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
exact hs hx