no goals
F : Type ?u.666981
α : Type u_1
β : Type ?u.666987
γ : Type ?u.666990
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : GroupWithZero α
s t : Finset α
hs : Finset.Nonempty s
⊢ 0 ⊆ 0 / s
simpa [mem_div] using hs