G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer H = H → H = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ NormalizerCondition G
rw [normalizerCondition_iff_only_full_group_self_normalizing]
case hbase

⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G] (H : Subgroup G), normalizer H = H → H = ⊤

case hstep

⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Group.IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer H = H → H = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer H = H → H = ⊤
apply @nilpotent_center_quotient_ind _ G _ _ <;> clear! G
case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : normalizer H = H
⊢ H = ⊤
case hbase

⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G] (H : Subgroup G), normalizer H = H → H = ⊤
intro G _ _ H _
no goals
case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : normalizer H = H
⊢ H = ⊤
exact @Subsingleton.elim _ Unique.instSubsingleton _ _
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
⊢ H = ⊤
case hstep

⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Group.IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer H = H → H = ⊤
intro G _ _ ih H hH
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
⊢ H = ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
⊢ H = ⊤
have hch : center G ≤ H := Subgroup.center_le_normalizer.trans (le_of_eq hH)
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
⊢ H = ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
⊢ H = ⊤
have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
⊢ H = ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
⊢ H = ⊤
have hsur : Function.Surjective (mk' (center G)) := surjective_quot_mk _
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
⊢ H = ⊤
let H' := H.map (mk' (center G))
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ H = ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤
have hH' : H'.normalizer = H' := by
  apply comap_injective hsur
  rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
  exact hH
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ H = ⊤
apply map_injective_of_ker_le (mk' (center G)) hkh le_top
no goals
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤
exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))
no goals
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
⊢ MonoidHom.ker (mk' (center G)) ≤ H
simpa using hch
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ comap (mk' (center G)) (normalizer H') = comap (mk' (center G)) H'
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer H' = H'
apply comap_injective hsur
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer H = H
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ comap (mk' (center G)) (normalizer H') = comap (mk' (center G)) H'
rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
no goals
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer H = H
exact hH