no goals
F : Type ?u.657730
α : Type u_1
β : Type ?u.657736
γ : Type ?u.657739
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s✝ t s : Finset α
⊢ 0 / s ⊆ 0
simp [subset_iff, mem_div]