no goals
F : Type ?u.924314
α : Type u_2
β : Type u_1
γ : Type ?u.924323
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
ht : Finset.Nonempty t
⊢ 0 ⊆ 0 • t
simpa [mem_smul] using ht