no goals
F : Type ?u.715334
α : Type u_2
β : Type u_1
γ : Type ?u.715343
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s s₁ s₂ t u : Finset β
a : α
b x : β
⊢ x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y = x
simp only [Finset.smul_finset_def, and_assoc, mem_image, exists_prop, Prod.exists, mem_product]