G : Type u_2
G' : Type ?u.390813
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.390822
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_1
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H) → ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
G : Type u_2
G' : Type ?u.390813
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.390822
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_1
inst✝ : Group N
f : N →* G
x : N
⊢ x ∈ comap f (normalizer H) → x ∈ normalizer (comap f H)
simp only [mem_normalizer_iff, mem_comap]
G : Type u_2
G' : Type ?u.390813
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.390822
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_1
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H
n : N
⊢ ↑f n ∈ H ↔ ↑f (x * n * x⁻¹) ∈ H
G : Type u_2
G' : Type ?u.390813
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.390822
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_1
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H) → ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
intro h n
no goals
G : Type u_2
G' : Type ?u.390813
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.390822
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_1
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H
n : N
⊢ ↑f n ∈ H ↔ ↑f (x * n * x⁻¹) ∈ H
simp [h (f n)]