G : Type u_1
G' : Type ?u.339502
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.339511
inst✝ : AddGroup A
H K : Subgroup G
nH : Normal H
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H
G : Type u_1
G' : Type ?u.339502
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.339511
inst✝ : AddGroup A
H K : Subgroup G
nH : Normal H
a b : G
h : a * b ∈ H
⊢ b * a ∈ H
have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
no goals
G : Type u_1
G' : Type ?u.339502
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.339511
inst✝ : AddGroup A
H K : Subgroup G
nH : Normal H
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H
simp_all only [inv_mul_cancel_left, inv_inv]