no goals
F : Type ?u.832295
α : Type u_2
β : Type u_1
γ : Type ?u.832304
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]