no goals
F : Type ?u.904200
α : Type u_1
β : Type u_2
γ : Type ?u.904209
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t : Finset β
s : Finset α
⊢ s • 0 ⊆ 0
simp [subset_iff, mem_smul]