no goals
G : Type u_2
G' : Type ?u.669539
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.669548
inst✝¹ : AddGroup A
N : Type u_1
inst✝ : Group N
H : Subgroup N
hH : Normal H
f : G →* N
x✝ : G
⊢ x✝ ∈ Subgroup.comap f H → ∀ (g : G), g * x✝ * g⁻¹ ∈ Subgroup.comap f H
simp (config := { contextual := true }) [Subgroup.mem_comap, hH.conj_mem]