no goals
G : Type u_1
G' : Type ?u.384795
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.384804
inst✝ : AddGroup A
H K : Subgroup G
x : G
hx : x ∈ center G
y : G
⊢ y ∈ H ↔ x * y * x⁻¹ ∈ H
simp [← mem_center_iff.mp hx y, mul_assoc]