G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : x ∈ normalizer (comap f H)
⊢ x ∈ comap f (normalizer H)
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
⊢ normalizer (comap f H) ≤ comap f (normalizer H)
intro x hx
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
⊢ ∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : x ∈ normalizer (comap f H)
⊢ x ∈ comap f (normalizer H)
simp only [mem_comap, mem_normalizer_iff] at *
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
n : G
⊢ n ∈ H ↔ ↑f x * n * (↑f x)⁻¹ ∈ H
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
⊢ ∀ (h : G), h ∈ H ↔ ↑f x * h * (↑f x)⁻¹ ∈ H
intro n
case intro
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
y : N
⊢ ↑f y ∈ H ↔ ↑f x * ↑f y * (↑f x)⁻¹ ∈ H
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
n : G
⊢ n ∈ H ↔ ↑f x * n * (↑f x)⁻¹ ∈ H
rcases hf n with ⟨y, rfl⟩
no goals
case intro
G : Type u_1
G' : Type ?u.618855
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.618864
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : N →* G
hf : Surjective ↑f
x : N
hx : ∀ (h : N), ↑f h ∈ H ↔ ↑f (x * h * x⁻¹) ∈ H
y : N
⊢ ↑f y ∈ H ↔ ↑f x * ↑f y * (↑f x)⁻¹ ∈ H
simp [hx y]