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