no goals
G : Type u_1
G' : Type ?u.385870
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.385879
inst✝ : AddGroup A
H K : Subgroup G
hK : Normal (subgroupOf H K)
HK : H ≤ K
x : G
hx : x ∈ K
y : G
yH : x * y * x⁻¹ ∈ H
⊢ y ∈ H
simpa [mem_subgroupOf, mul_assoc] using
  hK.conj_mem ⟨x * y * x⁻¹, HK yH⟩ yH ⟨x⁻¹, K.inv_mem hx⟩