no goals
G : Type u_1
G' : Type ?u.384241
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.384250
inst✝ : AddGroup A
H K : Subgroup G
h : Normal H
a : G
_ha : a ∈ ⊤
b : G
hb : a * b * a⁻¹ ∈ H
⊢ b ∈ H
rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb