awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
⊢ IsSolvable L
have obtain : ∀ (k : ℕ) (h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥), IsSolvable L
Tactic: obtain ⟨k, h⟩ : ∃ k, LieModule.lowerCentralSeries ℤ L L k = ⊥ := hL.nilpotent_int
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
⊢ IsSolvable L
have h₁ : Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
⊢ Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥
have h₁ : ∀ (h : LE.le (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥),
  LE.le (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥
Tactic: rw [← le_bot_iff] at h ⊢
Cleared hypotheses: h
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
have succ : Eq.{v + 1} (α := Submodule R (L ⧸ I))
  (Submodule.span R
    {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x})
  (Submodule.span R
    {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x})
Tactic: simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
⊢ Eq.{v + 1} (α := Submodule R (L ⧸ I))
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x})
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x})
have succ : Eq.{v + 1} (α := L ⧸ I → Prop)
  (fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x)
  fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
Tactic: congr
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
⊢ Eq.{v + 1} (α := L ⧸ I → Prop)
    (fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x)
    fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
have succ : ∀ (x : L ⧸ I),
  (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) ↔
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
Tactic: ext x
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
x : L ⧸ I
⊢ (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) ↔
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
have succ : (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) →
  ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
Tactic: constructor
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
x : L ⧸ I
succ :
  (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) →
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
⊢ (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) ↔
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
have succ₁ : (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x) →
  ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x
Tactic: constructor
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x : L ⧸ I), (↑n : L ⧸ I)⁆ = ⁅y, z⁆
have hz₁ : Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z
Tactic: rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
Cleared hypotheses: hz
-- 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
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
val : L ⧸ I
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x : L), (↑n : L ⧸ I)⁆ = ⁅y, z⁆
have hz₁ : Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z
Tactic: rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
Cleared hypotheses: hz
-- 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
I : LieIdeal R L
k : ℕ
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
have zero : Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) 0) : Submodule R (L ⧸ I))
  (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0) : Submodule R (L ⧸ I))
Tactic: induction k with
  | zero =>
    simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    congr
    ext x
    constructor
    · rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
    · rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
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
I : LieIdeal R L
k : ℕ
zero :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) 0) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0) : Submodule R (L ⧸ I))
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
have succ : ∀ (k : ℕ)
  (ih :
    Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
      (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))),
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
Tactic: induction k with
  | zero =>
    simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    congr
    ext x
    constructor
    · rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
    · rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
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
I : LieIdeal R L
k : ℕ
ih :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) (k + 1)) : Submodule R ↥I)
have succ : LE.le.{v} (α := Submodule R ↥I)
  (Submodule.span R {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (↥I) (↥I) k)), ⁅(↑x_1 : ↥I), (↑n : ↥I)⁆ = x})
  (Submodule.span R {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (↥I) k)), ⁅(↑x_1 : L), (↑n : ↥I)⁆ = x})
Tactic: simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
-- 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
I : LieIdeal R L
k : ℕ
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
have zero : LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) 0) : Submodule R ↥I)
  (↑(lowerCentralSeries R L (↥I) 0) : Submodule R ↥I)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    apply Submodule.span_mono
    rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
    exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩
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
I : LieIdeal R L
k : ℕ
zero :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) 0) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) 0) : Submodule R ↥I)
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
have succ : ∀ (k : ℕ)
  (ih :
    LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
      (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)),
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) (k + 1)) : Submodule R ↥I)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    apply Submodule.span_mono
    rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
    exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩
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
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
⊢ LieRing.IsNilpotent L
have suffices : LieModule.IsNilpotent L (L ⧸ I)
Tactic: suffices LieModule.IsNilpotent L (L ⧸ I) by
    exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
-- 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
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
⊢ LieModule.IsNilpotent L (L ⧸ I)
have simp : ∀ (h₂ : ∃ (k : ℕ), Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥),
  ∃ (k : ℕ), Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥
Tactic: simp only [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₂ ⊢
Cleared hypotheses: h₂
-- 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
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ (k : ℕ), Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥
have h : ∀ (k : ℕ) (hk : Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥),
  Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥
Tactic: peel h₂ with k hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f (lowerCentralSeries R L L (k + 1)) ≤ lowerCentralSeries R L' L' (k + 1)
have succ : map f (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k)) ≤
  Bracket.bracket (L := LieIdeal R L') ⊤ (lowerCentralSeries R L' L' k)
Tactic: simp only [LieModule.lowerCentralSeries_succ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
have zero : map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0
Tactic: induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ]
    exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
zero : map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
have succ : ∀ (k : ℕ) (ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k),
  map f (lowerCentralSeries R L L (k + 1)) ≤ lowerCentralSeries R L' L' (k + 1)
Tactic: induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ]
    exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ map f ⊤ = ⊤
have rw : f.idealRange = ⊤
Tactic: rw [← f.idealRange_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
have h' : map f ⊤ = ⊤
Tactic: have h' : (⊤ : LieIdeal R L).map f = ⊤ := by
    rw [← f.idealRange_eq_map]
    exact f.idealRange_eq_top_of_surjective h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
have zero : map f (lowerCentralSeries R L L 0) = lowerCentralSeries R L' L' 0
Tactic: induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero]; exact h'
  | succ k ih => simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h' : map f ⊤ = ⊤
zero : map f (lowerCentralSeries R L L 0) = lowerCentralSeries R L' L' 0
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
have succ : ∀ (k : ℕ) (ih : map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k),
  map f (lowerCentralSeries R L L (k + 1)) = lowerCentralSeries R L' L' (k + 1)
Tactic: induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero]; exact h'
  | succ k ih => simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : LieRing.IsNilpotent L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ LieRing.IsNilpotent L
have rw : ∀ (h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥) {f : L →ₗ⁅R⁆ L'}
  (h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')),
  ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
Tactic: rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢
Cleared hypotheses: h₁, f, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
have h : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥),
  Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
Tactic: peel h₁ with k hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
⊢ Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
have h : LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
Tactic: apply LieIdeal.bot_of_map_eq_bot h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
have h : LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
Tactic: rw [eq_bot_iff, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : LieRing.IsNilpotent L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ LieRing.IsNilpotent L'
have rw : ∀ (h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥) {f : L →ₗ⁅R⁆ L'}
  (h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')),
  ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
Tactic: rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢
Cleared hypotheses: h₁, f, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
have h : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥),
  Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
Tactic: peel h₁ with k hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
⊢ Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
have h : LieIdeal.map f ⊥ = ⊥
Tactic: rw [← LieIdeal.lowerCentralSeries_map_eq k h₂, hk]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
⊢ LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'
have mp : LieRing.IsNilpotent L → LieRing.IsNilpotent L'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
mp : LieRing.IsNilpotent L → LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'
have mpr : LieRing.IsNilpotent L' → LieRing.IsNilpotent L
Tactic: constructor
-- 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
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L)) ↔ LieRing.IsNilpotent L
have refine_1 : ∀ (h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))), LieRing.IsNilpotent L
Tactic: refine ⟨fun h => ?_, ?_⟩