-- Mathlib/GroupTheory/Nilpotent.lean
theorem normalizerCondition_of_isNilpotent [h : IsNilpotent G] : NormalizerCondition G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H'.normalizer = H'

Tactic:
apply comap_injective hsur

Result:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ comap (mk' (center G)) H'.normalizer = comap (mk' (center G)) H'

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
⊢ H = ⊤

Tactic:
have hkh : (mk' (center G)).ker ≤ H := by simpa using hch

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
⊢ H = ⊤

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
⊢ H = ⊤

Tactic:
let H' := H.map (mk' (center G))

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤

Proof state:
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ NormalizerCondition G

Tactic:
rw [normalizerCondition_iff_only_full_group_self_normalizing]

Result:
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
⊢ H = ⊤

Tactic:
have hch : center G ≤ H := Subgroup.center_le_normalizer.trans (le_of_eq hH)

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
⊢ H = ⊤

Proof state:
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤

Tactic:
apply @nilpotent_center_quotient_ind _ G _ _ <;> clear! G

Result:
case hbase

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

case hstep

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

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
⊢ H = ⊤

Tactic:
have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
⊢ H = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
⊢ (mk' (center G)).ker ≤ H

Tactic:
simpa using hch

Result:
no goals

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : H'.normalizer = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤

Tactic:
exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))

Result:
no goals

Proof state:
case hbase

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

Tactic:
intro G _ _ H _

Result:
case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : H.normalizer = H
⊢ H = ⊤

Proof state:
case hstep

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

Tactic:
intro G _ _ ih H hH

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
⊢ H = ⊤

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ comap (mk' (center G)) H'.normalizer = comap (mk' (center G)) H'

Tactic:
rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]

Result:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H.normalizer = H

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤

Tactic:
have hH' : H'.normalizer = H' := by
  apply comap_injective hsur
  rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
  exact hH

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : H'.normalizer = H'
⊢ H = ⊤

Proof state:
case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : H.normalizer = H
⊢ H = ⊤

Tactic:
exact @Subsingleton.elim _ Unique.instSubsingleton _ _

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H.normalizer = H

Tactic:
exact hH

Result:
no goals