awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
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)
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
⊢ Set.ncard (α := Subgroup G) (upperCentralSeries G '' Set.Iic a) = a + 1

Tactic:
refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_

Premises used: Set.ncard_eq_of_bijective, Subgroup.upperCentralSeries
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (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:
grind
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (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:
grind
-- Module: Mathlib.GroupTheory.Nilpotent
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

Tactic:
(upperCentralSeries.StrictMonoOn G).injOn ?_ ?_

Premises used: StrictMonoOn.injOn, Subgroup.upperCentralSeries.StrictMonoOn
-- Module: Mathlib.GroupTheory.Nilpotent
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)
refine_3₁ : j ∈ 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

Tactic:
refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_

Premises used: StrictMonoOn.injOn, Subgroup.upperCentralSeries.StrictMonoOn
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ i ∈ Set.Iic (nilpotencyClass G)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ j ∈ Set.Iic (nilpotencyClass G)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) 0)
    (prod (lowerCentralSeries G₁ 0) (lowerCentralSeries G₂ 0))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
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.succ)
    (Bracket.bracket (L := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊤)

Tactic:
rfl

Premises used: Set.Mem, setOf, Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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))
rw 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)) ⊤)
⊢ 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:
rw [ih]
-- Module: Mathlib.GroupTheory.Nilpotent
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₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) ⊤)
    (Bracket.bracket (L := Subgroup (G₁ × G₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) (prod ⊤ ⊤))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
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₂)) (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)) (prod ⊤ ⊤))
    (prod (Bracket.bracket (L := Subgroup G₁) (lowerCentralSeries G₁ n) ⊤)
      (Bracket.bracket (L := Subgroup G₂) (lowerCentralSeries G₂ n) ⊤))

Tactic:
(commutator_prod_prod _ _ _ _)

Premises used: Subgroup.commutator_prod_prod
-- Module: Mathlib.GroupTheory.Nilpotent
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₂))
    (prod (Bracket.bracket (L := Subgroup G₁) (lowerCentralSeries G₁ n) ⊤)
      (Bracket.bracket (L := Subgroup G₂) (lowerCentralSeries G₂ n) ⊤))
    (prod (lowerCentralSeries G₁ n.succ) (lowerCentralSeries G₂ n.succ))

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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)) ⊤)
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 ⊤ ⊤))
⊢ Eq (α := Subgroup (G₁ × G₂)) (Subgroup.lowerCentralSeries (G₁ × G₂) (n + 1))
    (prod (Subgroup.lowerCentralSeries G₁ (n + 1)) (Subgroup.lowerCentralSeries G₂ (n + 1)))

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

Premises used: Subgroup.commutator_prod_prod, Bracket.bracket, Subgroup.lowerCentralSeries, Subgroup.prod, Prod, Top.top, Nat.succ, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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))
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)))
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n)
    (prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n))

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

Premises used: Subgroup.commutator_prod_prod, Bracket.bracket, Subgroup.lowerCentralSeries, Subgroup.prod, Prod, Top.top, Nat.succ, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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 : ∃ (n : ℕ), Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊥
⊢ IsNilpotent (G₁ × G₂)

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
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) ⊥

Tactic:
⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩

Premises used: Group.nilpotencyClass, Max.max, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
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₂
refine : Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂))) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × G₂) n) ⊥

Tactic:
refine ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
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 ⊥ ⊥) ⊥
rw₃ rw₄ : Eq (α := Subgroup (G₁ × G₂)) ⊥ ⊥
⊢ Eq (α := Subgroup (G₁ × G₂)) (lowerCentralSeries (G₁ × 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]

Premises used: le_max_right, Iff.mpr, Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, Subgroup.lowerCentralSeries_prod, le_max_left, Subgroup.bot_prod_bot
-- Module: Mathlib.GroupTheory.Nilpotent
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₂)

Tactic:
eq_of_forall_ge_iff fun k => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsNilpotent G₁
inst_3 : IsNilpotent G₂
refine : ∀ (k : ℕ), nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
⊢ nilpotencyClass (G₁ × G₂) = max (nilpotencyClass G₁) (nilpotencyClass G₂)

Tactic:
refine eq_of_forall_ge_iff fun k => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsNilpotent G₁
inst_3 : IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k

Tactic:
simp only [max_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
    lowerCentralSeries_prod, prod_eq_bot_iff]

Premises used: Subgroup.prod_eq_bot_iff, max_le_iff, Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, Subgroup.lowerCentralSeries_prod
-- Module: Mathlib.GroupTheory.Nilpotent
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
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)

Tactic:
simp [pi_top]

Premises used: Subgroup.pi_top
-- Module: Mathlib.GroupTheory.Nilpotent
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)
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n.succ)
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊤)

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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))
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊤)
    ⁅pi fun (i : η) ↦ lowerCentralSeries (Gs i) n, ⊤⁆

Tactic:
commutator_mono ih (le_refl _)

Premises used: le_refl, Subgroup.commutator_mono
-- Module: Mathlib.GroupTheory.Nilpotent
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)
⊢ ⁅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)
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)
⊢ ⁅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_le _ _

Premises used: Set.Mem, setOf, Subgroup.commutator_pi_pi_le
-- Module: Mathlib.GroupTheory.Nilpotent
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)
⊢ (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)
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)) (Subgroup.lowerCentralSeries ((i : η) → Gs i) n)
    (Subgroup.pi (f := Gs) Set.univ 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 : η) ↦ ⊤⁆
⊢ LE.le (α := 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, ⊤⁆ := 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

Premises used: le_refl, Subgroup.commutator_mono, Bracket.bracket, Subgroup.commutator_pi_pi_le, Subgroup.lowerCentralSeries, Top.top, Nat.succ, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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)
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))
⊢ LE.le (α := 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, ⊤⁆ := 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

Premises used: Subgroup.pi_top, Bracket.bracket, Subgroup.commutator_pi_pi_le, Subgroup.lowerCentralSeries, Top.top, Nat.succ, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
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
rw : ∃ (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:
η : 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) ⊥

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
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
refine : Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
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
rw : LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
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
apply : LE.le (α := Subgroup ((i : η) → Gs i)) (pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n) ⊥
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊥

Tactic:
apply le_trans (lowerCentralSeries_pi_le _)

Premises used: Subgroup.lowerCentralSeries_pi_le, le_trans
-- Module: Mathlib.GroupTheory.Nilpotent
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
rw : ∀ (i : η), Eq.{u_3 + 1} (α := Subgroup (Gs i)) (lowerCentralSeries (Gs i) n) ⊥
⊢ LE.le (α := Subgroup ((i : η) → Gs i)) (pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) n) ⊥

Tactic:
rw [← eq_bot_iff, pi_eq_bot_iff]

Premises used: Subgroup.pi_eq_bot_iff, eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
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
i : η
⊢ Eq.{u_3 + 1} (α := Subgroup (Gs i)) (lowerCentralSeries (Gs i) n) ⊥

Tactic:
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (h i)

Premises used: Iff.mpr, Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
-- 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
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) 0)
    (Subgroup.pi (f := Gs) Set.univ fun (i : η) ↦ lowerCentralSeries (Gs i) 0)

Tactic:
simp [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)
⊢ Eq (α := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n.succ)
    (Bracket.bracket (L := Subgroup ((i : η) → Gs i)) (lowerCentralSeries ((i : η) → Gs i) n) ⊤)

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl