awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n - 1
have pos : ∀ (hn : nilpotencyClass G = 0),
  nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = HSub.hSub (α := ℕ) 0 1
Tactic: rcases n with (rfl | n)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
pos :
  ∀ (hn : nilpotencyClass G = 0),
    nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = HSub.hSub (α := ℕ) 0 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n - 1
have pos₁ : ∀ (n : ℕ) (hn : nilpotencyClass G = n + 1),
  nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n + 1 - 1
Tactic: rcases n with (rfl | n)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = HSub.hSub (α := ℕ) 0 1
have pos : ∀ (hn : Subsingleton G), Subsingleton.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
Tactic: simp only [nilpotencyClass_zero_iff_subsingleton, zero_tsub] at *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n + 1 - 1
have pos : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
Tactic: suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
have pos : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ≤ n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
pos : nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ≤ n
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n
have pos₁ : n ≤ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ≤ n
have pos : Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
  (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
Tactic: apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ Eq.{u_1 + 1} (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)))
    (upperCentralSeries (HasQuotient.Quotient G (B := Subgroup G) (center G)) n) ⊤
have pos : 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))
  (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ⊤)
Tactic: apply comap_injective (f := (mk' (center G))) Quot.mk_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ 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))
    (comap (N := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ⊤)
have pos : Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
Tactic: rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
have pos : n + 1 ≤ nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) + 1
Tactic: apply le_of_add_le_add_right
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) + 1
have rw : nilpotencyClass G = nilpotencyClass G - 1 + 1
Tactic: rw [nilpotencyClass_quotient_center]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1
have zero : ∀ (h : nilpotencyClass G = 0), 0 = HSub.hSub (α := ℕ) 0 1 + 1
Tactic: rcases h : Group.nilpotencyClass G with ⟨⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
zero : ∀ (h : nilpotencyClass G = 0), 0 = HSub.hSub (α := ℕ) 0 1 + 1
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1
have succ : ∀ (n : ℕ) (h : nilpotencyClass G = n + 1), n + 1 = n + 1 - 1 + 1
Tactic: rcases h : Group.nilpotencyClass G with ⟨⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = HSub.hSub (α := ℕ) 0 1 + 1
have zero : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
hH : IsNilpotent G
inst_1 : Nontrivial G
h : nilpotencyClass G = 0
⊢ False
have h₁ : Subsingleton G
Tactic: rw [nilpotencyClass_zero_iff_subsingleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
⊢ P G
have obtain : ∀ (n : ℕ) (h : nilpotencyClass G = n), P G
Tactic: obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = 0
⊢ P G
have zero : ∀ (this : Subsingleton G), P G
Tactic: haveI := nilpotencyClass_zero_iff_subsingleton.mp h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ P G
have succ : ∀ (hn : nilpotencyClass.{u_2} (HasQuotient.Quotient G (B := Subgroup G) (center G)) = n), P G
Tactic: have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
h : nilpotencyClass G = n
⊢ P G
have zero : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = 0), P G
Tactic: induction n generalizing G with
  | zero =>
    haveI := nilpotencyClass_zero_iff_subsingleton.mp h
    exact hbase _
  | succ n ih =>
    have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
    exact hstep _ (ih _ hn)
Cleared hypotheses: G, inst, inst_1, n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst : Group G
inst_1 : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G
hstep :
  ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G],
    P (HasQuotient.Quotient G (B := Subgroup G) (center G)) → P G
n : ℕ
h : nilpotencyClass G = n
zero : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = 0), P G
⊢ P G
have succ : ∀ (n : ℕ) (ih : ∀ (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n), P G)
  (G : Type u_2) [inst : Group G] [inst_2 : IsNilpotent G] (h : nilpotencyClass G = n + 1), P G
Tactic: induction n generalizing G with
  | zero =>
    haveI := nilpotencyClass_zero_iff_subsingleton.mp h
    exact hbase _
  | succ n ih =>
    have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
    exact hstep _ (ih _ hn)
Cleared hypotheses: G, inst, inst_1, n, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
i : ℕ
ih : LE.le (α := Subgroup G) (derivedSeries G i) (lowerCentralSeries G i)
⊢ LE.le (α := Subgroup G) (derivedSeries G (i + 1)) (lowerCentralSeries G (i + 1))
have succ : LE.le (α := Subgroup G) (derivedSeries G i) ⊤
Tactic: apply commutator_mono ih
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)
have zero : LE.le (α := Subgroup G) (derivedSeries G 0) (lowerCentralSeries G 0)
Tactic: induction n with
  | zero => simp
  | succ i ih => apply commutator_mono ih; simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero : LE.le (α := Subgroup G) (derivedSeries G 0) (lowerCentralSeries G 0)
⊢ LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)
have succ : ∀ (i : ℕ) (ih : LE.le (α := Subgroup G) (derivedSeries G i) (lowerCentralSeries G i)),
  LE.le (α := Subgroup G) (derivedSeries G (i + 1)) (lowerCentralSeries G (i + 1))
Tactic: induction n with
  | zero => simp
  | succ i ih => apply commutator_mono ih; simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
H : Subgroup G_1
inst_1 : H.Normal
G : Type u_2
inst_2 : CommGroup G
⊢ Group.IsNilpotent G
have h : Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤
Tactic: use 1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
H : Subgroup G_1
inst_1 : H.Normal
G : Type u_2
inst_2 : CommGroup G
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤
have h : Eq (α := Subgroup G) (center G) ⊤
Tactic: rw [upperCentralSeries_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : CommGroup G
⊢ nilpotencyClass G ≤ 1
have rw : Eq (α := Subgroup G) (center G) ⊤
Tactic: rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
inst_2 : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ Eq (α := Subgroup G) (center G) ⊤
have rw : Eq (α := Subgroup G) (upperCentralSeries G 1) ⊤
Tactic: rw [← upperCentralSeries_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a ≤ b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
have refine : ∀ (n : ℕ) (hmn : a ≤ n),
  Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G n) →
    Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (n + 1))
Tactic: refine Nat.le_induction rfl ?_ b ab
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G c)
have refine_1 : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
Tactic: refine eq_ge_of_eq_succ ac (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
refine_1 : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G (a + 1))
⊢ Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G c)
have refine_2 : LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G a)
Tactic: refine eq_ge_of_eq_succ ac (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b c : ℕ
ab : a < b
ac : a ≤ c
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G a)
have refine_2 : LE.le (α := Subgroup G) (upperCentralSeries G (a + 1)) (upperCentralSeries G b)
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ nilpotencyClass G ≤ a
have pos : ∀ (hG : Group.IsNilpotent G), nilpotencyClass G ≤ a
Tactic: by_cases hG : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
pos : ∀ (hG : Group.IsNilpotent G), nilpotencyClass G ≤ a
⊢ nilpotencyClass G ≤ a
have neg : ∀ (hG : ¬Group.IsNilpotent G), nilpotencyClass G ≤ a
Tactic: by_cases hG : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a b : ℕ
ab : a < b
hn : Eq (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a
have neg : 0 ≤ a
Tactic: rw [nilpotencyClass_of_not_nilpotent hG]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
have pos : ∀ (hG : Group.IsNilpotent G), _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
Tactic: by_cases hG : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
pos :
  ∀ (hG : Group.IsNilpotent G),
    _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
have neg : ∀ (hG : ¬Group.IsNilpotent G),
  _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
Tactic: by_cases hG : IsNilpotent G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a : ℕ
ha : a ∈ Set.Iic (nilpotencyClass G)
b : ℕ
hb : b ∈ Set.Iic (nilpotencyClass G)
ab : a < b
⊢ LT.lt (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
have ha₁ : a ≤ nilpotencyClass G
Tactic: simp only [Set.mem_Iic] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a : ℕ
ha : a ∈ Set.Iic (nilpotencyClass G)
b : ℕ
hb : b ∈ Set.Iic (nilpotencyClass G)
ab : a < b
ha₁ : a ≤ nilpotencyClass G
⊢ LT.lt (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
have hb₁ : b ≤ nilpotencyClass G
Tactic: simp only [Set.mem_Iic] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ LT.lt (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
have pos : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
pos : LE.le (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
⊢ LT.lt (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
have pos₁ : Ne (α := Subgroup G) (upperCentralSeries G a) (upperCentralSeries G b)
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
have neg : _root_.StrictMonoOn (β := Subgroup G) (upperCentralSeries G) {⊥}
Tactic: rw [nilpotencyClass_of_not_nilpotent hG, ← Nat.bot_eq_zero, Set.Iic_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ Set.ncard (α := Subgroup G) (upperCentralSeries G '' Set.Iic a) = a + 1
have refine_1 : ∀ (a_1 : Subgroup G),
  Membership.mem (γ := Set (Subgroup G)) (upperCentralSeries G '' Set.Iic a) a_1 →
    ∃ (i : ℕ) (h : i < a + 1), (fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i h = a_1
Tactic: refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
refine_1 :
  ∀ (a_1 : Subgroup G),
    Membership.mem (γ := Set (Subgroup G)) (upperCentralSeries G '' Set.Iic a) a_1 →
      ∃ (i : ℕ) (h : i < a + 1), (fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i h = a_1
⊢ Set.ncard (α := Subgroup G) (upperCentralSeries G '' Set.Iic a) = a + 1
have refine_2 : ∀ (i : ℕ) (h : i < a + 1),
  Membership.mem (γ := Set (Subgroup G)) (upperCentralSeries G '' Set.Iic a)
    ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i h)
Tactic: refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
refine_1 :
  ∀ (a_1 : Subgroup G),
    Membership.mem (γ := Set (Subgroup G)) (upperCentralSeries G '' Set.Iic a) a_1 →
      ∃ (i : ℕ) (h : i < a + 1), (fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i h = a_1
refine_2 :
  ∀ (i : ℕ) (h : i < a + 1),
    Membership.mem (γ := Set (Subgroup G)) (upperCentralSeries G '' Set.Iic a)
      ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i h)
⊢ Set.ncard (α := Subgroup G) (upperCentralSeries G '' Set.Iic a) = a + 1
have refine_3 : ∀ (i j : ℕ) (hi : i < a + 1) (hj : j < a + 1),
  Eq.{u_1 + 1} (α := Subgroup G) ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i hi)
      ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) j hj) →
    i = j
Tactic: refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i hi)
      ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) j hj) →
    i = j
have refine_3 : i ∈ Set.Iic (nilpotencyClass G)
Tactic: refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
refine_3 : i ∈ Set.Iic (nilpotencyClass G)
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) i hi)
      ((fun (x : ℕ) (x_1 : x < a + 1) ↦ (upperCentralSeries G x : Subgroup G)) j hj) →
    i = j
have refine_3₁ : j ∈ Set.Iic (nilpotencyClass G)
Tactic: refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
n : ℕ
ih :
  Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n)
    (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n))
⊢ Eq (α := Subgroup (G₁ × G₂)) (Bracket.bracket (L := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊤)
    (Bracket.bracket (L := Subgroup (G₁ × G₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) ⊤)
have rw : Eq (α := Subgroup (G₁ × G₂))
  (Bracket.bracket (L := Subgroup (G₁ × G₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) ⊤)
  (Bracket.bracket (L := Subgroup (G₁ × G₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) ⊤)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
n : ℕ
ih :
  Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n)
    (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n))
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (n + 1))
    (prod (lowerCentralSeries G₁ (n + 1)) (lowerCentralSeries G₂ (n + 1)))
have lowerCentralSeries : Eq (α := Subgroup (G₁ × G₂)) (Bracket.bracket (L := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊤)
  (Bracket.bracket (L := Subgroup (G₁ × G₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) ⊤)
Tactic: calc
      lowerCentralSeries (G₁ × G₂) n.succ = ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ := rfl
      _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ := by rw [ih]
      _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), (⊤ : Subgroup G₁).prod ⊤⁆ := by
        simp
      _ = ⁅lowerCentralSeries G₁ n, (⊤ : Subgroup G₁)⁆.prod ⁅lowerCentralSeries G₂ n, ⊤⁆ :=
        (commutator_prod_prod _ _ _ _)
      _ = (lowerCentralSeries G₁ n.succ).prod (lowerCentralSeries G₂ n.succ) := rfl