awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
n : ℕ
ih :
  Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
rw rw₁ :
  Eq (α := Subgroup ((i : η) → Gs i))
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i))
      (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n) ⊤)
    ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆
⊢ Eq (α := Subgroup ((i : η) → Gs i))
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊤)
    ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆

Tactic:
rw [ih]
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
n : ℕ
ih :
  Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
⊢ ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆ = ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, pi fun (i : η) ↦ ⊤⁆

Tactic:
simp [pi, pi_top]

Premises used: Subgroup.pi_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
n : ℕ
ih :
  Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
⊢ ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, pi fun (i : η) ↦ ⊤⁆ =
    pi fun (i : η) ↦ Bracket.bracket (L := Subgroup (Gs i)) (lowerCentralSeries (Gs i) n) ⊤

Tactic:
commutator_pi_pi_of_finite _ _

Premises used: Set.Mem, setOf, Subgroup.commutator_pi_pi_of_finite
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
n : ℕ
ih :
  Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
⊢ (pi fun (i : η) ↦ Bracket.bracket (L := Subgroup (Gs i)) (lowerCentralSeries (Gs i) n) ⊤) =
    pi fun (i : η) ↦ lowerCentralSeries (Gs i) n.succ

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
n : ℕ
ih :
  Eq (α := Subgroup ((i : η) → Gs i)) (Subgroup.lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n)
lowerCentralSeries :
  Eq (α := Subgroup ((i : η) → Gs i))
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (Subgroup.lowerCentralSeries ((i : η) → Gs i) n) ⊤)
    ⁅pi fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n, ⊤⁆
lowerCentralSeries₁ :
  ⁅pi fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n, ⊤⁆ =
    ⁅pi fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n, pi fun (i : η) ↦ ⊤⁆
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (Subgroup.lowerCentralSeries ((i : η) → Gs i) (n + 1))
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) (n + 1))

Tactic:
calc
      lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
      _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := by rw [ih]
      _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi, pi_top]
      _ = pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := commutator_pi_pi_of_finite _ _
      _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl

Premises used: Bracket.bracket, Subgroup.lowerCentralSeries, Top.top, Nat.succ, Subgroup.commutator_pi_pi_of_finite, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Finite η
n : ℕ
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
zero :
  Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)
succ :
  ∀ (n : ℕ)
    (ih :
      Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
        (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)),
    Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) (n + 1))
      (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) (n + 1))
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)

Tactic:
induction n with
  | zero => simp [pi_top]
  | succ n ih =>
    calc
      lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
      _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := by rw [ih]
      _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi, pi_top]
      _ = pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := commutator_pi_pi_of_finite _ _
      _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl

Premises used: Subgroup.pi_top, Bracket.bracket, Subgroup.lowerCentralSeries, Top.top, Nat.succ, Subgroup.commutator_pi_pi_of_finite, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
intro : ∀ (val : Fintype η), IsNilpotent ((i : η) → Gs i)
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
cases nonempty_fintype η

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
intro : ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
rw [nilpotent_iff_lowerCentralSeries]

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
⊢ ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥

Tactic:
⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), ?_⟩

Premises used: Finset.univ, Group.nilpotencyClass, Exists.intro, Finset.sup
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
intro :
  Eq (α := Subgroup ((i : η) → Gs i))
    (lowerCentralSeries ((i : η) → Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥

Tactic:
refine ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
intro :
  ∀ (i : η),
    Eq.{u_3 + 1} (α := Subgroup (Gs i))
      (lowerCentralSeries (Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥
⊢ Eq (α := Subgroup ((i : η) → Gs i))
    (lowerCentralSeries ((i : η) → Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥

Tactic:
rw [lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]

Premises used: Subgroup.pi_eq_bot_iff, Subgroup.lowerCentralSeries_pi_of_finite
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
i : η
intro : nilpotencyClass.{u_3} (Gs i) ≤ Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)
⊢ Eq.{u_3 + 1} (α := Subgroup (Gs i))
    (lowerCentralSeries (Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥

Tactic:
rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]

Premises used: Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
i : η
⊢ nilpotencyClass.{u_3} (Gs i) ≤ Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)

Tactic:
Finset.le_sup (f := fun i => Group.nilpotencyClass (Gs i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
η : Type u_2
Gs : η → Type u_3
inst_2 : (i : η) → Group (Gs i)
inst_3 : Finite η
inst_4 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
val : Fintype η
i : η
⊢ nilpotencyClass.{u_3} (Gs i) ≤ Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)

Tactic:
exact Finset.le_sup (f := fun i => Group.nilpotencyClass (Gs i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Fintype η
inst_2 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
H :
  ∀ (c : ℕ),
    nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)) ≤ c
⊢ nilpotencyClass ((i : η) → Gs i) = Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)

Tactic:
apply eq_of_forall_ge_iff

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Fintype η
inst_2 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)) ≤ k

Tactic:
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
    lowerCentralSeries_pi_of_finite, pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]

Premises used: Finset.mem_univ, Subgroup.pi_eq_bot_iff, true_imp_iff, Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, Subgroup.lowerCentralSeries_pi_of_finite, Finset.sup_le_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥), IsSolvable G
⊢ IsSolvable G

Tactic:
obtain ⟨n, hn⟩ := nilpotent_iff_lowerCentralSeries.1 h

Premises used: Subgroup.nilpotent_iff_lowerCentralSeries, Iff.mp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
h₁ : Eq (α := Subgroup G) (derivedSeries G n) ⊥
⊢ IsSolvable G

Tactic:
use n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
h₁ : LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)
⊢ Eq (α := Subgroup G) (derivedSeries G n) ⊥

Tactic:
rw [eq_bot_iff, ← hn]

Premises used: eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)

Tactic:
derived_le_lower_central n

Premises used: Subgroup.derived_le_lower_central
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)

Tactic:
exact derived_le_lower_central n

Premises used: Subgroup.derived_le_lower_central
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : IsSimpleGroup G
inst_3 : Group.IsNilpotent G
⊢ IsCyclic G

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
inst_2 : IsNilpotent G
⊢ nilpotencyClass G ≤ 1

Tactic:
CommGroup.nilpotencyClass_le_one

Premises used: CommGroup.nilpotencyClass_le_one
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent G
rw : ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ NormalizerCondition G

Tactic:
rw [normalizerCondition_iff_only_full_group_self_normalizing]

Premises used: normalizerCondition_iff_only_full_group_self_normalizing
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent G
hbase : ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
hstep :
  ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
        normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
      ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
apply @nilpotent_center_quotient_ind _ G _ _

Premises used: Group.nilpotent_center_quotient_ind
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hbase : ∀ [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hbase : ∀ [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : Subsingleton G
H : Subgroup G
hbase : normalizer (↑H : Set G) = H → H = ⊤
⊢ normalizer (↑H : Set G) = H → H = ⊤

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : Subsingleton G
H : Subgroup G
h : normalizer (↑H : Set G) = H
⊢ H = ⊤

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

Premises used: Subsingleton.elim
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : Subsingleton G
H : Subgroup G
h : normalizer (↑H : Set G) = H
⊢ H = ⊤

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

Premises used: Subsingleton.elim
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hstep :
  ∀ [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
        normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
      ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
        normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
      ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hstep :
  ∀ [IsNilpotent G],
    (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
        normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
      ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ [IsNilpotent G],
    (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
        normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
      ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
⊢ center G ≤ H

Tactic:
have hch : center G ≤ H := Subgroup.center_le_normalizer H |>.trans (le_of_eq hH)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
⊢ MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H

Tactic:
simpa using hch
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
⊢ MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H

Tactic:
have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
⊢ Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)

Tactic:
have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
a : comap (mk' (center G)) (normalizer (↑H' : Set (G ⧸ center G))) = comap (mk' (center G)) H'
⊢ normalizer (↑H' : Set (G ⧸ center G)) = H'

Tactic:
apply comap_injective hsur

Premises used: Subgroup.comap_injective
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
a : normalizer (↑H : Set G) = H
⊢ comap (mk' (center G)) (normalizer (↑H' : Set (G ⧸ center G))) = comap (mk' (center G)) H'

Tactic:
rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]

Premises used: Subgroup.comap_normalizer_eq_of_surjective, Subgroup.comap_map_eq_self
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
⊢ normalizer (↑H : Set G) = H

Tactic:
hH
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
⊢ normalizer (↑H : Set G) = H

Tactic:
exact hH
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
⊢ normalizer (↑H' : Set (G ⧸ center G)) = H'

Tactic:
have hH' : normalizer H' = H' := by
      apply comap_injective hsur
      rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
      exact hH
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
hH' : normalizer (↑H' : Set (G ⧸ center G)) = H'
hstep :
  Eq (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))) (Subgroup.map (mk' (center G)) H)
    (Subgroup.map (mk' (center G)) ⊤)
⊢ H = ⊤

Tactic:
apply map_injective_of_ker_le (mk' (center G)) hkh le_top

Premises used: Subgroup.map_injective_of_ker_le, Subgroup.center, QuotientGroup.mk', le_top