case a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ map f (comap f (normalizer H)) = map f (normalizer (comap f H))
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ comap f (normalizer H) = normalizer (comap f H)
apply Subgroup.map_injective hf
case a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H = map f (normalizer (comap f H))
case a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ map f (comap f (normalizer H)) = map f (normalizer (comap f H))
rw [map_comap_eq_self h]
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H ≤ map f (normalizer (comap f H))

case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ map f (normalizer (comap f H)) ≤ normalizer H
case a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H = map f (normalizer (comap f H))
apply le_antisymm
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H = map f (comap f (normalizer H))
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H ≤ map f (normalizer (comap f H))
refine' le_trans (le_of_eq _) (map_mono (le_normalizer_comap _))
no goals
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer H = map f (comap f (normalizer H))
rw [map_comap_eq_self h]
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer (map f (comap f H)) = normalizer H
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ map f (normalizer (comap f H)) ≤ normalizer H
refine' le_trans (le_normalizer_map f) (le_of_eq _)
no goals
case a.a
G : Type u_2
G' : Type ?u.624266
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.624275
inst✝² : AddGroup A
N✝ : Type ?u.624281
inst✝¹ : Group N✝
f✝ : G →* N✝
N : Type u_1
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ↑f
h : normalizer H ≤ range f
⊢ normalizer (map f (comap f H)) = normalizer H
rw [map_comap_eq_self (le_trans le_normalizer h)]