no goals
F : Type ?u.929758
α : Type u_2
β : Type u_1
γ : Type ?u.929767
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMulWithZero α β
inst✝ : DecidableEq β
s✝ : Finset α
t s : Finset β
h : Finset.Nonempty s
⊢ ↑(0 • s) = ↑0
simpa using @Set.zero_smul_set α _ _ _ _ _ h