no goals
F : Type ?u.599923
α : Type u_1
β : Type ?u.599929
γ : Type ?u.599932
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ 0 * s
simpa [mem_mul] using hs