rw [Set.mem_smul_set_iff_inv_smul_mem]
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ a⁻¹ • x✝ ∈ ↑s ↔ x✝ ∈ ↑s