G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  Normal (normalizer ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))) →
    Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))
⊢ normalizer (normalizer ↑P) = normalizer ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ normalizer (normalizer ↑P) = normalizer ↑P
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ normalizer (normalizer ↑P) = normalizer ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  Normal (normalizer ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))) →
    Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))
⊢ normalizer (normalizer ↑P) = normalizer ↑P
simp_rw [← normalizer_eq_top, Sylow.coe_subtype, ← subgroupOf_normalizer_eq le_normalizer, ←
  subgroupOf_normalizer_eq le_rfl, subgroupOf_self] at this
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ Subgroup.map (Subgroup.subtype (normalizer (normalizer ↑P)))
      (subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P))) =
    normalizer ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ normalizer (normalizer ↑P) = normalizer ↑P
rw [← subtype_range (P : Subgroup G).normalizer.normalizer, MonoidHom.range_eq_map,
  ← this trivial]
no goals
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ Subgroup.map (Subgroup.subtype (normalizer (normalizer ↑P)))
      (subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P))) =
    normalizer ↑P
exact map_comap_eq_self (le_normalizer.trans (ge_of_eq (subtype_range _)))