no goals
F : Type ?u.935966
α : Type u_1
β : Type u_2
γ : Type ?u.935975
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : NoZeroSMulDivisors α β
a : α
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]