no goals
G : Type u_1
G' : Type ?u.383552
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.383561
inst✝ : AddGroup A
H K : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n * x⁻¹ ∈ H
rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]