no goals
G : Type u_1
H : Type ?u.59591
A : Type ?u.59594
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
g : G
hg : g ∈ s
n : G
⊢ n ∈ s ↔ g * n * g⁻¹ ∈ s
rw [IsSubgroup.mul_mem_cancel_right hs ((IsSubgroup.inv_mem_iff hs).2 hg),
  IsSubgroup.mul_mem_cancel_left hs hg]