no goals
G : Type u_1
H : Type ?u.18673
A : Type ?u.18676
a a₁ a₂ b c : G
inst✝ : CommGroup G
s : Set G
hs : IsSubgroup s
n : G
hn : n ∈ s
g : G
⊢ g * n * g⁻¹ ∈ s
rwa [mul_right_comm, mul_right_inv, one_mul]