case hf
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ Injective ↑(Subgroup.subtype N)

case h
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ normalizer H ≤ range (Subgroup.subtype N)
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ subgroupOf (normalizer H) N = normalizer (subgroupOf H N)
apply comap_normalizer_eq_of_injective_of_le_range
case h
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ normalizer H ≤ range (Subgroup.subtype N)
case hf
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ Injective ↑(Subgroup.subtype N)

case h
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ normalizer H ≤ range (Subgroup.subtype N)
exact Subtype.coe_injective
no goals
case h
G : Type u_1
G' : Type ?u.626768
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.626777
inst✝¹ : AddGroup A
N✝ : Type ?u.626783
inst✝ : Group N✝
f : G →* N✝
H N : Subgroup G
h : normalizer H ≤ N
⊢ normalizer H ≤ range (Subgroup.subtype N)
simpa