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