awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)) (Subgroup.lowerCentralSeries (G₁ × G₂) n)
    (prod (Subgroup.lowerCentralSeries G₁ n) (Subgroup.lowerCentralSeries G₂ n))
lowerCentralSeries :
  Eq (α := Subgroup (G₁ × G₂)) (Bracket.bracket (L := Subgroup (G₁ × G₂)) (Subgroup.lowerCentralSeries (G₁ × G₂) n) ⊤)
    (Bracket.bracket (L := Subgroup (G₁ × G₂))
      (prod (Subgroup.lowerCentralSeries G₁ n) (Subgroup.lowerCentralSeries G₂ n)) ⊤)
⊢ Eq (α := Subgroup (G₁ × G₂)) (Subgroup.lowerCentralSeries (G₁ × G₂) (n + 1))
    (prod (Subgroup.lowerCentralSeries G₁ (n + 1)) (Subgroup.lowerCentralSeries G₂ (n + 1)))
have lowerCentralSeries₁ : Eq (α := Subgroup (G₁ × G₂))
  (Bracket.bracket (L := Subgroup (G₁ × G₂))
    (prod (Subgroup.lowerCentralSeries G₁ n) (Subgroup.lowerCentralSeries G₂ n)) ⊤)
  (Bracket.bracket (L := Subgroup (G₁ × G₂))
    (prod (Subgroup.lowerCentralSeries G₁ n) (Subgroup.lowerCentralSeries G₂ n)) (prod ⊤ ⊤))
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
-- 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 : ℕ
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n)
    (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n))
have zero : Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) 0) (prod (lowerCentralSeries G₁ 0) (lowerCentralSeries G₂ 0))
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    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
Cleared hypotheses: n
-- 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 : ℕ
zero :
  Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) 0)
    (prod (lowerCentralSeries G₁ 0) (lowerCentralSeries G₂ 0))
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n)
    (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n))
have succ : ∀ (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)))
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
⊢ IsNilpotent (G₁ × G₂)
have rw : ∃ (n : ℕ), Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊥
Tactic: rw [nilpotent_iff_lowerCentralSeries]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
⊢ ∃ (n : ℕ), Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊥
have refine : Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
Tactic: refine ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
have rw : Eq (α := Subgroup (G₁ × G₂))
  (prod (lowerCentralSeries G₁ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))
    (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂))))
  ⊥
Tactic: rw [lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
rw :
  Eq (α := Subgroup (G₁ × G₂))
    (prod (lowerCentralSeries G₁ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))
      (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂))))
    ⊥
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
have rw₁ : Eq (α := Subgroup (G₁ × G₂)) (prod ⊥ (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))) ⊥
Tactic: rw [lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
rw :
  Eq (α := Subgroup (G₁ × G₂))
    (prod (lowerCentralSeries G₁ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))
      (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂))))
    ⊥
rw₁ : Eq (α := Subgroup (G₁ × G₂)) (prod ⊥ (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))) ⊥
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
have rw₂ : Eq (α := Subgroup (G₁ × G₂)) (prod ⊥ ⊥) ⊥
Tactic: rw [lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsNilpotent G₁
inst_5 : IsNilpotent G₂
rw :
  Eq (α := Subgroup (G₁ × G₂))
    (prod (lowerCentralSeries G₁ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))
      (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂))))
    ⊥
rw₁ : Eq (α := Subgroup (G₁ × G₂)) (prod ⊥ (lowerCentralSeries G₂ (max (nilpotencyClass G₁) (nilpotencyClass G₂)))) ⊥
rw₂ : Eq (α := Subgroup (G₁ × G₂)) (prod ⊥ ⊥) ⊥
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
have rw₃ : Eq (α := Subgroup (G₁ × G₂)) ⊥ ⊥
Tactic: rw [lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
-- 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₂
inst_2 : IsNilpotent G₁
inst_3 : IsNilpotent G₂
⊢ nilpotencyClass (G₁ × G₂) = max (nilpotencyClass G₁) (nilpotencyClass G₂)
have refine : ∀ (k : ℕ), nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
Tactic: refine eq_of_forall_ge_iff fun k => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
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 :
  LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) (n + 1))
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) (n + 1))
have lowerCentralSeries : ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆ = ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, pi fun (i : η) ↦ ⊤⁆
Tactic: calc
      lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
      _ ≤ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := commutator_mono ih (le_refl _)
      _ = ⁅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_le _ _
      _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
n : ℕ
pi : (f : (i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) :=
  fun (f : (i : η) → Subgroup (Gs i)) ↦ Subgroup.pi (f := Gs) Set.univ f
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
have zero : LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
  (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)
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, ⊤⁆ := commutator_mono ih (le_refl _)
      _ = ⁅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_le _ _
      _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
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 :
  LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
have succ : ∀ (n : ℕ)
  (ih :
    LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
      (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)),
  LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) (n + 1))
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) (n + 1))
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, ⊤⁆ := commutator_mono ih (le_refl _)
      _ = ⁅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_le _ _
      _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass.{u_3} (Gs i) ≤ n
⊢ IsNilpotent ((i : η) → Gs i)
have rw : ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
Tactic: rw [nilpotent_iff_lowerCentralSeries]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass.{u_3} (Gs i) ≤ n
⊢ ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
have refine : Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass.{u_3} (Gs i) ≤ n
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
have rw : LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass.{u_3} (Gs i) ≤ n
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
have apply : LE.le (α := Subgroup ((i : η) → Gs i)) (pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n) ⊥
Tactic: apply le_trans (lowerCentralSeries_pi_le _)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass.{u_3} (Gs i) ≤ n
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n) ⊥
have rw : ∀ (i : η), Eq.{u_3 + 1} (α := Subgroup (Gs i)) (lowerCentralSeries (Gs i) n) ⊥
Tactic: rw [← eq_bot_iff, pi_eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ Eq (α := Subgroup ((i : η) → Gs i))
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊤)
    ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆
have 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, ⊤⁆
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) (n + 1))
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) (n + 1))
have lowerCentralSeries : 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: 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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, ⊤⁆
⊢ 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))
have lowerCentralSeries₁ : ⁅pi fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n, ⊤⁆ =
  ⁅pi fun (i : η) ↦ Subgroup.lowerCentralSeries (Gs i) n, pi fun (i : η) ↦ ⊤⁆
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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
have zero : Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
  (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n)
have 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))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ IsNilpotent ((i : η) → Gs i)
have intro : ∀ (val : Fintype η), IsNilpotent ((i : η) → Gs i)
Tactic: cases nonempty_fintype η
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 η
⊢ IsNilpotent ((i : η) → Gs i)
have intro : ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
Tactic: rw [nilpotent_iff_lowerCentralSeries]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊥
have intro : Eq (α := Subgroup ((i : η) → Gs i))
  (lowerCentralSeries ((i : η) → Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥
Tactic: refine ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 η
⊢ Eq (α := Subgroup ((i : η) → Gs i))
    (lowerCentralSeries ((i : η) → Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥
have intro : ∀ (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_pi_of_finite, pi_eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 : η
⊢ Eq.{u_3 + 1} (α := Subgroup (Gs i))
    (lowerCentralSeries (Gs i) (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i))) ⊥
have intro : nilpotencyClass.{u_3} (Gs i) ≤ Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)
Tactic: rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
η : Type u_2
Gs : η → Type u_3
inst : (i : η) → Group (Gs i)
inst_1 : Fintype η
inst_2 : ∀ (i : η), IsNilpotent.{u_3} (Gs i)
⊢ nilpotencyClass ((i : η) → Gs i) = Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)
have H : ∀ (c : ℕ),
  nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.sup Finset.univ fun (i : η) ↦ nilpotencyClass.{u_3} (Gs i)) ≤ c
Tactic: apply eq_of_forall_ge_iff
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
⊢ IsSolvable G
have obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥), IsSolvable G
Tactic: obtain ⟨n, hn⟩ := nilpotent_iff_lowerCentralSeries.1 h