no goals
α : Type ?u.162017
G : Type u_1
A : Type ?u.162023
S : Type ?u.162026
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_right (inv_mem hh)]