no goals
F : Type ?u.581097
α : Type u_1
β : Type ?u.581103
γ : Type ?u.581106
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : MulZeroClass α
s✝ t s : Finset α
⊢ s * 0 ⊆ 0
simp [subset_iff, mem_mul]