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
inst_6 : LieModule R L M
x y : L
m : M
k : ℕ
zero :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (HMul.hMul (α := ℕ) 2 0))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[0]
      m)
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
have succ : ∀ (k : ℕ)
  (ih :
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
      ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
                ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
            (a : M) → M)^[k]
        m)),
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * (k + 1)))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k + 1]
      m)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]
    refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) 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
k_1 : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)
have succ : Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M k)) ≤
  Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ k)
Tactic: simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
-- 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
have zero : LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0
Tactic: induction k with
  | zero => simp only [lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    exact LieSubmodule.mono_lie_right ⊤ 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
zero : LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
have succ : ∀ (k : ℕ) (ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k),
  LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)
Tactic: induction k with
  | zero => simp only [lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    exact LieSubmodule.mono_lie_right ⊤ 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k
have apply : lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
Tactic: apply le_antisymm (map_lowerCentralSeries_le k f)
-- 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
have zero : ⊤ ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
Tactic: rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : ⊤ ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
have zero₁ : ⊤ ≤ LieSubmodule.map f ⊤
Tactic: rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : ⊤ ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
zero₁ : ⊤ ≤ LieSubmodule.map f ⊤
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
have zero₂ : LieSubmodule.map f ⊤ = ⊤
Tactic: rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : ⊤ ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
zero₁ : ⊤ ≤ LieSubmodule.map f ⊤
zero₂ : LieSubmodule.map f ⊤ = ⊤
⊢ lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
have zero₃ : f.range = ⊤
Tactic: rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
n : ℕ
h : lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n)
⊢ lowerCentralSeries R L M₂ (n + 1) ≤ LieSubmodule.map f (lowerCentralSeries R L M (n + 1))
have succ : Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M₂ n) ≤
  Bracket.bracket.{v, w₁} (L := LieIdeal R L) ⊤ (LieSubmodule.map f (lowerCentralSeries R L M n))
Tactic: simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
-- 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
have zero : lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
Tactic: induction k with
  | zero =>
    rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_eq_top]
  | succ =>
    simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    apply LieSubmodule.mono_lie_right
    assumption
-- 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
k : ℕ
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
zero : lowerCentralSeries R L M₂ 0 ≤ LieSubmodule.map f (lowerCentralSeries R L M 0)
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
have succ : ∀ (n : ℕ),
  lowerCentralSeries R L M₂ n ≤ LieSubmodule.map f (lowerCentralSeries R L M n) →
    lowerCentralSeries R L M₂ (n + 1) ≤ LieSubmodule.map f (lowerCentralSeries R L M (n + 1))
Tactic: induction k with
  | zero =>
    rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top,
      f.range_eq_top]
  | succ =>
    simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    apply LieSubmodule.mono_lie_right
    assumption
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
have zero : LE.le (α := LieIdeal R L) (derivedSeriesOfIdeal R L 0 ⊤) (lowerCentralSeries R L L 0)
Tactic: rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
zero : LE.le (α := LieIdeal R L) (derivedSeriesOfIdeal R L 0 ⊤) (lowerCentralSeries R L L 0)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
have zero₁ : LE.le (α := LieIdeal R L) ⊤ (lowerCentralSeries R L L 0)
Tactic: rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
zero : LE.le (α := LieIdeal R L) (derivedSeriesOfIdeal R L 0 ⊤) (lowerCentralSeries R L L 0)
zero₁ : LE.le (α := LieIdeal R L) ⊤ (lowerCentralSeries R L L 0)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
have zero₂ : LE.le.{v} (α := LieIdeal R L) ⊤ ⊤
Tactic: rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L (k + 1)) (lowerCentralSeries R L L (k + 1))
have h' : LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤
Tactic: have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
h' : LE.le (α := LieIdeal R L) (derivedSeries R L k) ⊤
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L (k + 1)) (lowerCentralSeries R L L (k + 1))
have succ : LE.le (α := LieIdeal R L)
  (Bracket.bracket (L := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊤) (derivedSeriesOfIdeal R L k ⊤))
  (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k))
Tactic: rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
have zero : LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
Tactic: induction k with
  | zero => rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
  | succ k h =>
    have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
    rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
    exact LieSubmodule.mono_lie h' h
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
zero : LE.le (α := LieIdeal R L) (derivedSeries R L 0) (lowerCentralSeries R L L 0)
⊢ LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)
have succ : ∀ (k : ℕ) (h : LE.le (α := LieIdeal R L) (derivedSeries R L k) (lowerCentralSeries R L L k)),
  LE.le (α := LieIdeal R L) (derivedSeries R L (k + 1)) (lowerCentralSeries R L L (k + 1))
Tactic: induction k with
  | zero => rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
  | succ k h =>
    have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
    rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
    exact LieSubmodule.mono_lie h' h
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
inst_7 : IsNilpotent L M
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent 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
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) ⊥
have rw : LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M k)
Tactic: rw [eq_bot_iff, ← 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
N : LieSubmodule R L M
⊢ IsNilpotent.{v, w} L ↥N ↔ ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥
have rw : (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥) ↔
  ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥
Tactic: rw [isNilpotent_iff R L N]
-- 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
N : LieSubmodule R L M
⊢ (∃ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥) ↔
    ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥
have refine : ∀ (k : ℕ), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥
Tactic: refine exists_congr fun 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
N : LieSubmodule R L M
k : ℕ
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥
have rw : LieSubmodule.comap N.incl (LieSubmodule.lcs k N) = ⊥ ↔ LieSubmodule.lcs k N = ⊥
Tactic: rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
    inf_eq_right.mpr (N.lcs_le_self 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
N : LieSubmodule R L M
k : ℕ
rw : LieSubmodule.comap N.incl (LieSubmodule.lcs k N) = ⊥ ↔ LieSubmodule.lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥
have rw₁ : N ⊓ LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
Tactic: rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
    inf_eq_right.mpr (N.lcs_le_self 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
N : LieSubmodule R L M
k : ℕ
rw : LieSubmodule.comap N.incl (LieSubmodule.lcs k N) = ⊥ ↔ LieSubmodule.lcs k N = ⊥
rw₁ : N ⊓ LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ LieSubmodule.lcs k N = ⊥
have rw₂ : LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥
Tactic: rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
    inf_eq_right.mpr (N.lcs_le_self 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
k : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst_6 : AddCommGroup M₂
inst_7 : Module R M₂
inst_8 : LieRingModule L M₂
inst_9 : LieModule R L M₂
inst_10 : LieModule R L M
inst_11 : IsTrivial L M
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) ⊥
have h : Eq (α := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M 1) ⊥
Tactic: use 1
-- 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
k : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
have obtain : ∀ (k : ℕ) (hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥),
  IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent 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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
have obtain : ∀ (l : ℕ) (hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥),
  IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
Tactic: obtain ⟨l, hl⟩ := IsNilpotent.nilpotent 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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
have h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
Tactic: have h₁ : lowerCentralSeries R L M₁ (k ⊔ l) = ⊥ := lcs_eq_bot M₁ (Nat.le_max_left k l) 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
k_1 : ℕ
N : LieSubmodule R L M
M₂_1 : Type w₁
inst_6 : AddCommGroup M₂_1
inst_7 : Module R M₂_1
inst_8 : LieRingModule L M₂_1
inst_9 : LieModule R L M₂_1
inst_10 : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst_11 : IsNilpotent.{v, w} L ↥M₁
inst_12 : IsNilpotent.{v, w} L ↥M₂
k : ℕ
hk : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) k) ⊥
l : ℕ
hl : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) l) ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M) (le : m ≤ n)
  (hn : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) m) ⊥),
  Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) n) ⊥ :=
  ⋯
h₁ : Eq.{w + 1} (α := LieSubmodule R L ↥M₁) (lowerCentralSeries R L (↥M₁) (max k l)) ⊥
⊢ IsNilpotent.{v, w} L ↥(M₁ ⊔ M₂)
have h₂ : Eq.{w + 1} (α := LieSubmodule R L ↥M₂) (lowerCentralSeries R L (↥M₂) (max k l)) ⊥
Tactic: have h₂ : lowerCentralSeries R L M₂ (k ⊔ l) = ⊥ := lcs_eq_bot M₂ (Nat.le_max_right k l) hl