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