G : Type u_1
G' : Type ?u.714616
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.714625
inst✝¹ : AddGroup A
N : Type ?u.714631
inst✝ : Group N
H K : Subgroup G
hK : H ≤ K
hN : Normal (subgroupOf H K)
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
⊢ b * a ∈ H
G : Type u_1
G' : Type ?u.714616
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.714625
inst✝¹ : AddGroup A
N : Type ?u.714631
inst✝ : Group N
H K : Subgroup G
hK : H ≤ K
hN : Normal (subgroupOf H K)
a b : G
hb : b ∈ K
h : a * b ∈ H
⊢ b * a ∈ H
have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
no goals
G : Type u_1
G' : Type ?u.714616
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.714625
inst✝¹ : AddGroup A
N : Type ?u.714631
inst✝ : Group N
H K : Subgroup G
hK : H ≤ K
hN : Normal (subgroupOf H K)
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
⊢ b * a ∈ H
rwa [mul_assoc, mul_assoc, mul_right_inv, mul_one] at this