awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
⊢ False
have this : LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
Tactic: have : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M :=
    le_inf_iff.mpr ⟨lowerCentralSeriesLast_le_of_not_isTrivial R L M contra,
      lowerCentralSeriesLast_le_max_triv 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
inst_7 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
⊢ False
have suffices : ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
Tactic: suffices ¬ Nontrivial (lowerCentralSeriesLast R L M) by
    exact this (nontrivial_lowerCentralSeriesLast R 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 : IsNilpotent L M
h : Disjoint (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
h_1 : Nontrivial M
contra : ¬IsTrivial L M
this :
  LE.le (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) (lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M)
⊢ ¬Nontrivial.{w} ↥(lowerCentralSeriesLast R L M)
have this₁ : Eq (α := LieSubmodule R L M) (lowerCentralSeriesLast R L M) ⊥
Tactic: rw [h.eq_bot, le_bot_iff] at this
Cleared hypotheses: this
-- 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 : ℕ
ih :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M (k + 1)) : Submodule R M)
    (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
have succ : Eq.{w + 1} (α := Submodule R M)
  (Submodule.span R
    {x : M |
      ∃ (x_1 : ↥(LieHom.range (toEnd R L M))),
        Membership.mem (γ := LieIdeal R ↥(LieHom.range (toEnd R L M))) ⊤ x_1 ∧
          ∃ (n : M),
            Membership.mem (γ := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) n ∧ ⁅x_1, n⁆ = x})
  (Submodule.span R
    {x : M |
      ∃ (x_1 : L),
        Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
          ∃ (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x})
Tactic: simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
-- 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 : ℕ
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)
have zero : Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M 0) : Submodule R M)
  (↑(lowerCentralSeries R L M 0) : Submodule R M)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
    simp
Cleared hypotheses: 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 : ℕ
zero :
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M 0) : Submodule R M)
    (↑(lowerCentralSeries R L M 0) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑(lowerCentralSeries R L M k) : Submodule R M)
have succ : ∀ (k : ℕ)
  (ih :
    Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
      (↑(lowerCentralSeries R L M k) : Submodule R M)),
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M (k + 1)) : Submodule R M)
    (↑(lowerCentralSeries R L M (k + 1)) : Submodule R M)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
    simp
Cleared hypotheses: 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
⊢ IsNilpotent (↥(LieHom.range (toEnd R L M))) M ↔ IsNilpotent L M
have simp : (∃ (k : ℕ),
    Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
      (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) ↔
  ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: simp only [isNilpotent_iff R _ 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 : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) ↔
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have mp : (∃ (k : ℕ),
    Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
      (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) →
  ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: constructor
-- 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
mp :
  (∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) →
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ (∃ (k : ℕ),
      Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
        (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥) ↔
    ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have mpr : (∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥) →
  ∃ (k : ℕ),
    Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
      (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥
Tactic: constructor
-- 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 : ℕ
hk :
  Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
Tactic: use 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 : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ),
    Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M)
      (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥
have h : Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) ⊥
Tactic: use 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 : ℕ
hk :
  Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
have h : ∀
  (hk :
    Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
      (↑⊥ : Submodule R M)),
  Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)
Tactic: rw [← LieSubmodule.toSubmodule_inj] at hk ⊢
Cleared hypotheses: 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
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq (α := LieSubmodule R (↥(LieHom.range (toEnd R L M))) M) (lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k)
    ⊥
have h : ∀ (hk : Eq (α := Submodule R M) (↑(lowerCentralSeries R L M k) : Submodule R M) (↑⊥ : Submodule R M)),
  Eq (α := Submodule R M) (↑(lowerCentralSeries R (↥(LieHom.range (toEnd R L M))) M k) : Submodule R M)
    (↑⊥ : Submodule R M)
Tactic: rw [← LieSubmodule.toSubmodule_inj] at hk ⊢
Cleared hypotheses: 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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (k + 1) N₁ ≤ ucs (k + 1) N₂
have succ : (ucs k N₁).normalizer ≤ (ucs k N₂).normalizer
Tactic: simp only [ucs_succ]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂
have zero : ucs 0 N₁ ≤ ucs 0 N₂
Tactic: induction k with
  | zero => simpa
  | succ k ih =>
    simp only [ucs_succ]
    gcongr
Cleared hypotheses: 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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
h : N₁ ≤ N₂
zero : ucs 0 N₁ ≤ ucs 0 N₂
⊢ ucs k N₁ ≤ ucs k N₂
have succ : ∀ (k : ℕ) (ih : ucs k N₁ ≤ ucs k N₂), ucs (k + 1) N₁ ≤ ucs (k + 1) N₂
Tactic: induction k with
  | zero => simpa
  | succ k ih =>
    simp only [ucs_succ]
    gcongr
Cleared hypotheses: 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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
ih : ucs k N₁ = N₁
⊢ ucs (k + 1) N₁ = N₁
have succ : (ucs k N₁).normalizer = N₁
Tactic: rwa [ucs_succ, ih]
-- 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 : N₁.normalizer = N₁
k : ℕ
⊢ ucs k N₁ = N₁
have zero : ucs 0 N₁ = N₁
Tactic: induction k with
  | zero => simp
  | succ k ih => rwa [ucs_succ, ih]
Cleared hypotheses: 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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
zero : ucs 0 N₁ = N₁
⊢ ucs k N₁ = N₁
have succ : ∀ (k : ℕ) (ih : ucs k N₁ = N₁), ucs (k + 1) N₁ = N₁
Tactic: induction k with
  | zero => simp
  | succ k ih => rwa [ucs_succ, ih]
Cleared hypotheses: 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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ N₁
have rw : ucs k ⊥ ≤ ucs k N₁
Tactic: rw [← ucs_eq_self_of_normalizer_eq_self h 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
N₁ : LieSubmodule R L M
inst_6 : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ ucs k N₁
have h₁ : ⊥ ≤ N₁
Tactic: gcongr
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have rw : l + (k + 1) = l + 1 + k
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have succ₁ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₁ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have succ₂ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₁ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₂ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have succ₃ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs l N₁) ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
rw : l + (k + 1) = l + 1 + k
succ : lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₁ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
succ₂ : lcs (l + 1) N₁ ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
succ₃ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs l N₁) ≤ ucs k N₂ ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
have succ₄ : lcs l N₁ ≤ (ucs k N₂).normalizer ↔ lcs l N₁ ≤ (ucs k N₂).normalizer
Tactic: rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
-- 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₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
l k : ℕ
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
have zero : ∀ (l : ℕ), lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂
Tactic: induction k generalizing l with
  | zero => simp
  | succ k ih =>
    rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
Cleared hypotheses: l, 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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
l k : ℕ
zero : ∀ (l : ℕ), lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
have succ : ∀ (k : ℕ) (ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂) (l : ℕ),
  lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
Tactic: induction k generalizing l with
  | zero => simp
  | succ k ih =>
    rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
Cleared hypotheses: l, 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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂
have h : k = 0 + k
Tactic: convert! lcs_add_le_iff (R := R) (L := L) (M := M) 0 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
N₁ N₂ : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
⊢ k = 0 + k
have h : k = k
Tactic: rw [zero_add]
-- 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
k : ℕ
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N
have rw : lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
Tactic: rw [eq_top_iff, ← lcs_le_iff]
-- 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
⊢ LieModule.IsNilpotent L M ↔ ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤
have rw : (∃ (k : ℕ), Eq (α := LieSubmodule R L M) (LieModule.lowerCentralSeries R L M k) ⊥) ↔
  ∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L M) (ucs k ⊥) ⊤
Tactic: rw [LieModule.isNilpotent_iff R]
-- 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
k : ℕ
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥
have zero : comap N.incl (ucs 0 ⊥) = ucs 0 ⊥
Tactic: induction k with
  | zero => exact N.ker_incl
  | succ k ih => simp [← ih]
Cleared hypotheses: 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
zero : comap N.incl (ucs 0 ⊥) = ucs 0 ⊥
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥
have succ : ∀ (k : ℕ) (ih : comap N.incl (ucs k ⊥) = ucs k ⊥), comap N.incl (ucs (k + 1) ⊥) = ucs (k + 1) ⊥
Tactic: induction k with
  | zero => exact N.ker_incl
  | succ k ih => simp [← ih]
Cleared hypotheses: 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
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ LieModule.IsNilpotent.{v, w} L ↥N ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
have simp_rw : (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (ucs k ⊥) ⊤) ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
Tactic: simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top R, ← ucs_comap_incl, comap_incl_eq_top]
-- 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
simp_rw : (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (ucs k ⊥) ⊤) ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
⊢ LieModule.IsNilpotent.{v, w} L ↥N ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
have simp_rw₁ : (∃ (k : ℕ), comap N.incl (ucs k ⊥) = ⊤) ↔ ∃ (k : ℕ), N ≤ ucs k ⊥
Tactic: simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top R, ← ucs_comap_incl, comap_incl_eq_top]