awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : IsNilpotent.{v, w} L (M ⧸ N)
⊢ ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N
have obtain : ∀ (k : ℕ) (hk : lowerCentralSeries R L M k ≤ N), ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N
Tactic: obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ s.Nonempty
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥), s.Nonempty
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M
have hs : s.Nonempty
Tactic: have hs : s.Nonempty := by
    obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M
    exact ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M
have change : sInf s = 0 ↔ Subsingleton M
Tactic: change sInf s = 0 ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Subsingleton M
have rw : sInf s = 0 ↔ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
Tactic: rw [← LieSubmodule.subsingleton_iff ℤ L M, ← subsingleton_iff_bot_eq_top, ←
    lowerCentralSeries_zero, @eq_comm (LieSubmodule ℤ L M)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
have refine : ∀ (h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥), sInf s = 0
Tactic: refine ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
hs : s.Nonempty
h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥
⊢ sInf s = 0
have rw : 0 ∈ s ∨ s = ∅
Tactic: rw [Nat.sInf_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
⊢ nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥ ∧
      Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have aux : ∀ (k : ℕ),
  Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
    Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
Tactic: have aux (k : ℕ) : lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥ := by
    simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) ⊥ ∧
      Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have rw : nilpotencyLength L M = k + 1 ↔
  Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M (k + 1)) ⊥ ∧
    ¬Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
Tactic: rw [aux, ne_eq, aux]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ nilpotencyLength L M = k + 1 ↔
    Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M (k + 1)) ⊥ ∧
      ¬Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
have change : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
Tactic: change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
aux :
  ∀ (k : ℕ),
    Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥ ↔
      Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
s : Set ℕ := {k : ℕ | Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
Tactic: have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := by
    rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries ℤ L M k₁ = ⊥)
    exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Nontrivial M
⊢ nilpotencyLength L M = 1 ↔ IsTrivial L M
have rw : IsTrivial L M ∧ Ne (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 0) ⊥ ↔ IsTrivial L M
Tactic: rw [nilpotencyLength_eq_succ_iff ℤ, ← trivial_iff_lower_central_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
⊢ IsTrivial L M
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
h_1 : Nontrivial M
⊢ IsTrivial L M
have inl : ∀ (h : nilpotencyLength L M = 0), IsTrivial L M
Tactic: rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
h_1 : Nontrivial M
inl : ∀ (h : nilpotencyLength L M = 0), IsTrivial L M
⊢ IsTrivial L M
have inr : ∀ (h : nilpotencyLength L M = 1), IsTrivial L M
Tactic: rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h_1 : nilpotencyLength L M ≤ 1
h_2 : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M
have h₁ : Subsingleton M
Tactic: rw [nilpotencyLength_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : IsNilpotent L M
h_1 : nilpotencyLength L M ≤ 1
h_2 : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M
have inr : ∀ (h : IsTrivial L M), IsTrivial L M
Tactic: rwa [nilpotencyLength_eq_one_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (maxTrivSubmodule R L M)
have rw : LE.le.{w} (α := LieSubmodule R L M)
  (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k :
    LieSubmodule R L M)
  (maxTrivSubmodule R L M : LieSubmodule R L M)
Tactic: rw [lowerCentralSeriesLast]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
have zero : ∀ (h : nilpotencyLength L M = 0),
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
Tactic: rcases h : nilpotencyLength L M with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
zero :
  ∀ (h : nilpotencyLength L M = 0),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (maxTrivSubmodule R L M : LieSubmodule R L M)
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
have succ : ∀ (k : ℕ) (h : nilpotencyLength L M = k + 1),
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
Tactic: rcases h : nilpotencyLength L M with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
h : nilpotencyLength L M = k + 1
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (maxTrivSubmodule R L M : LieSubmodule R L M)
have succ : Eq.{w + 1} (α := LieSubmodule R L M)
  (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
      (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k) :
    LieSubmodule R L M)
  (⊥ : LieSubmodule R L M)
Tactic: rw [le_max_triv_iff_bracket_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
h : nilpotencyLength L M = k + 1
⊢ Eq.{w + 1} (α := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
        (match (motive := ℕ → LieSubmodule R L M) k + 1 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k) :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have h₁ : Eq (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) ⊥ ∧
  Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: rw [nilpotencyLength_eq_succ_iff R, lowerCentralSeries_succ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
⊢ Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
have rw : Ne.{w + 1} (α := LieSubmodule R L M)
  (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k :
    LieSubmodule R L M)
  (⊥ : LieSubmodule R L M)
Tactic: rw [LieSubmodule.nontrivial_iff_ne_bot, lowerCentralSeriesLast]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have zero : ∀ (h : nilpotencyLength L M = 0),
  Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
Tactic: cases h : nilpotencyLength L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
zero :
  ∀ (h : nilpotencyLength L M = 0),
    Ne.{w + 1} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (⊥ : LieSubmodule R L M)
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have succ : ∀ (n : ℕ) (h : nilpotencyLength L M = n + 1),
  Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) n + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
Tactic: cases h : nilpotencyLength L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
h : nilpotencyLength L M = 0
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have h₁ : ¬Nontrivial M
Tactic: rw [nilpotencyLength_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Nontrivial M
inst_8 : IsNilpotent L M
n : ℕ
h : nilpotencyLength L M = n + 1
⊢ Ne.{w + 1} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) n + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have h₁ : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (n + 1)) ⊥ ∧
  Ne (α := LieSubmodule R L M) (lowerCentralSeries R L M n) ⊥
Tactic: rw [nilpotencyLength_eq_succ_iff R] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : ¬IsTrivial L M
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1)
have rw : LE.le.{w} (α := LieSubmodule R L M)
  (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k :
    LieSubmodule R L M)
  (lowerCentralSeries R L M 1 : LieSubmodule R L M)
Tactic: rw [lowerCentralSeriesLast]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : ¬IsTrivial L M
⊢ 1 < nilpotencyLength L M
have by_contra : ∀ (contra : ¬1 < nilpotencyLength L M), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : ¬IsTrivial L M
contra : ¬1 < nilpotencyLength L M
⊢ False
have this : IsTrivial L M
Tactic: have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : ¬IsTrivial L M
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
have h₁ : 1 < nilpotencyLength L M
Tactic: replace h : 1 < nilpotencyLength L M := by
    by_contra contra
    have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
    contradiction
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : 1 < nilpotencyLength L M
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
have zero : ∀ (hk : nilpotencyLength L M = 0),
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
Tactic: rcases hk : nilpotencyLength L M with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : 1 < nilpotencyLength L M
zero :
  ∀ (hk : nilpotencyLength L M = 0),
    LE.le.{w} (α := LieSubmodule R L M)
      (match (motive := ℕ → LieSubmodule R L M) 0 with
        | 0 => ⊥
        | k.succ => lowerCentralSeries R L M k :
        LieSubmodule R L M)
      (lowerCentralSeries R L M 1 : LieSubmodule R L M)
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) nilpotencyLength L M with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
have succ : ∀ (k : ℕ) (hk : nilpotencyLength L M = k + 1),
  LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
Tactic: rcases hk : nilpotencyLength L M with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : 1 < nilpotencyLength L M
hk : nilpotencyLength L M = 0
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) 0 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
have h₁ : LT.lt (α := ℕ) 1 0
Tactic: rw [hk] at h
Cleared hypotheses: h, hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsNilpotent L M
h : 1 < nilpotencyLength L M
k : ℕ
hk : nilpotencyLength L M = k + 1
⊢ LE.le.{w} (α := LieSubmodule R L M)
    (match (motive := ℕ → LieSubmodule R L M) k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k :
      LieSubmodule R L M)
    (lowerCentralSeries R L M 1 : LieSubmodule R L M)
have h₁ : 1 < k + 1
Tactic: rw [hk] at h
Cleared hypotheses: h, hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
⊢ Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M
have refine : ∀ (h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)), IsTrivial L M
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
⊢ IsTrivial L M
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
⊢ IsTrivial L M
have by_contra : ∀ (contra : ¬IsTrivial L M), False
Tactic: by_contra contra