no goals
α : Type ?u.47334
G : Type u_1
A : Type ?u.47340
S : Type ?u.47343
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ : Set G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
simp [preimage_preimage, mul_assoc]