no goals
α : Type ?u.166670
G : Type u_1
A : Type ?u.166676
S : Type ?u.166679
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
H : Subgroup G
h : G
hh : h ∈ H
this : {x | x ∈ H} = ↑H
⊢ {h} * ↑H = ↑H
simpa [preimage, mul_mem_cancel_left (inv_mem hh)]