awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : Group.IsNilpotent H
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have rcases : ∀ (n : ℕ) (hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥),
  ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: rcases nilpotent_iff_lowerCentralSeries.mp ‹_› with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : Group.IsNilpotent H
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have h : Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : Group.IsNilpotent H
n : ℕ
hn : Eq (α := Subgroup H) (lowerCentralSeries H n) ⊥
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1)) ⊥
have h : map f (lowerCentralSeries G n) = ⊥
Tactic: refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
have this : IsNilpotent G
Tactic: have : IsNilpotent G := isNilpotent_of_ker_le_center f hf1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) sorry ≤ nilpotencyClass H + 1
Tactic: rw [← lowerCentralSeries_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ nilpotencyClass H + 1
have h : Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥
Tactic: apply Nat.find_min'
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) ⋯ ≤ nilpotencyClass H + 1
have h : Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥
Tactic: classical apply Nat.find_min'
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (nilpotencyClass H + 1)) ⊥
have h : map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
Tactic: refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
have h : map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst_2 : IsNilpotent H
this : IsNilpotent G
⊢ map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
have h : LE.le (α := Subgroup H) (lowerCentralSeries H (nilpotencyClass H)) ⊥
Tactic: apply le_trans (lowerCentralSeries.map f _)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
h : IsNilpotent G
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ IsNilpotent G'
have rcases : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤), IsNilpotent G'
Tactic: rcases h with ⟨n, hn⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ IsNilpotent G'
have h : Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
have h : LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)
Tactic: apply eq_top_iff.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ map f ⊤ = map f (upperCentralSeries G n)
have rw : map f ⊤ = map f ⊤
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)
have symm : map f ⊤ = map f (upperCentralSeries G n)
Tactic: calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G
have this : IsNilpotent G'
Tactic: have := nilpotent_of_surjective _ hf
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
⊢ nilpotencyClass G' ≤ nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) sorry ≤
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry
Tactic: rw [nilpotencyClass_def, nilpotencyClass_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯
have h₁ : ∀ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
Tactic: apply Nat.find_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤) ⋯ ≤
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯
have h₁ : ∀ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
Tactic: classical apply Nat.find_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Eq (α := Subgroup G') (upperCentralSeries G' n) ⊤
have h₁ : LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ map f ⊤ = map f (upperCentralSeries G n)
have rw : map f ⊤ = map f ⊤
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ LE.le (α := Subgroup G') ⊤ (upperCentralSeries G' n)
have symm : map f ⊤ = map f (upperCentralSeries G n)
Tactic: calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
inst_1 : H₁.Normal
inst_2 : H₂.Normal
h : H₁ = H₂
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))
have subst : ∀ [inst_3 : H₁.Normal], comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))
Tactic: subst h
Cleared hypotheses: H₂, inst_2, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
⊢ comap (mk' (center G)) Hn.upperCentralSeriesStep =
    comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))
have rw : comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn))) =
  comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))
Tactic: rw [upperCentralSeriesStep_eq_comap_center]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
Hn : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) :=
  upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) (n + 1)))
    (upperCentralSeries G (n + 1).succ)
have comap : comap (mk' (center G)) Hn.upperCentralSeriesStep =
  comap (mk' (center G)) (comap (mk' Hn) (center (HasQuotient.Quotient G (B := Subgroup G) (center G) ⧸ Hn)))
Tactic: calc
      comap (mk' (center G)) (upperCentralSeriesStep Hn) =
          comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) := by
        rw [upperCentralSeriesStep_eq_comap_center]
      _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
        QuotientGroup.comap_comap_center
      _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
        (comap_center_subst ih)
      _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
        symm (upperCentralSeriesStep_eq_comap_center _)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
have zero : Eq (α := Subgroup G)
  (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) 0))
  (upperCentralSeries G (Nat.succ 0))
Tactic: induction n with
  | zero =>
    simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
      (upperCentralSeries_one G).symm]
  | succ n ih =>
    let Hn := upperCentralSeries (G ⧸ center G) n
    calc
      comap (mk' (center G)) (upperCentralSeriesStep Hn) =
          comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) := by
        rw [upperCentralSeriesStep_eq_comap_center]
      _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
        QuotientGroup.comap_comap_center
      _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
        (comap_center_subst ih)
      _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
        symm (upperCentralSeriesStep_eq_comap_center _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero :
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) 0))
    (upperCentralSeries G (Nat.succ 0))
⊢ Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
    (upperCentralSeries G n.succ)
have succ : ∀ (n : ℕ)
  (ih :
    Eq (α := Subgroup G)
      (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
        (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n))
      (upperCentralSeries G n.succ)),
  Eq (α := Subgroup G)
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) (n + 1)))
    (upperCentralSeries G (n + 1).succ)
Tactic: induction n with
  | zero =>
    simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
      (upperCentralSeries_one G).symm]
  | succ n ih =>
    let Hn := upperCentralSeries (G ⧸ center G) n
    calc
      comap (mk' (center G)) (upperCentralSeriesStep Hn) =
          comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) := by
        rw [upperCentralSeriesStep_eq_comap_center]
      _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
        QuotientGroup.comap_comap_center
      _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
        (comap_center_subst ih)
      _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
        symm (upperCentralSeriesStep_eq_comap_center _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry = 0 ↔ Subsingleton G
Tactic: rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
Tactic: rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
Tactic: rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
Tactic: rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₄ : Subsingleton G ↔ Subsingleton G
Tactic: rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry = 0 ↔ Subsingleton G
Tactic: classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
Tactic: classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
Tactic: classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
Tactic: classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
rw : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ = 0 ↔ Subsingleton G
rw₁ : Eq (α := Subgroup G) (upperCentralSeries G 0) ⊤ ↔ Subsingleton G
rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊤ ↔ Subsingleton G
rw₃ : Subsingleton.{u_1 + 1} (Subgroup G) ↔ Subsingleton G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
have rw₄ : Subsingleton G ↔ Subsingleton G
Tactic: classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ IsNilpotent G
have obtain : ∀ (n : ℕ)
  (hn :
    Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
      (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤),
  IsNilpotent G
Tactic: obtain ⟨n, hn⟩ := h.nilpotent
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
n : ℕ
hn :
  Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
⊢ IsNilpotent G
have h₁ : Eq (α := Subgroup G) (upperCentralSeries G n.succ) ⊤
Tactic: use n.succ
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
have pos : ∀ (hH : IsNilpotent G),
  nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
Tactic: by_cases hH : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
pos :
  ∀ (hH : IsNilpotent G),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
have neg : ∀ (hH : ¬IsNilpotent G),
  nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
Tactic: by_cases hH : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
have neg : ¬IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
Tactic: rw [nilpotencyClass_of_not_nilpotent hH, zero_tsub, nilpotencyClass_of_not_nilpotent]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = nilpotencyClass G - 1
have pos : ∀ (n : ℕ) (hn : nilpotencyClass G = n),
  nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n - 1
Tactic: generalize hn : Group.nilpotencyClass G = n