awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) x
have zero : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x
zero : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) x
have add : ∀ (y z : M) (hy₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) y)
  (hz₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) z)
  (hy₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) y)
  (hz₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) z),
  Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (y + z)
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x
zero : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0
add :
  ∀ (y z : M) (hy₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) y)
    (hz₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) z)
    (hy₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) y)
    (hz₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) z),
    Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (y + z)
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) x
have smul_mem : ∀ (c : R₁) (y : M) (hy : y ∈ S), Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • y)
Tactic: induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩
Cleared hypotheses: hx
-- 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 :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ (↑(↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M (k + 1)) : Submodule ℤ M) : Set M)
have succ : (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) : Submodule R M) : Set M) =
  (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal ℤ L) ⊤ (lowerCentralSeries ℤ L M k)) : Submodule ℤ M) : Set M)
Tactic: rw [lowerCentralSeries_succ, lowerCentralSeries_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
inst_6 : LieModule R L M
k : ℕ
ih :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) : Submodule R M) : Set M) =
    (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal ℤ L) ⊤ (lowerCentralSeries ℤ L M k)) : Submodule ℤ M) : Set M)
have succ : (↑(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}) :
    Set M) =
  (↑(Submodule.span ℤ
        {x : M |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
              ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M)
Tactic: rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
-- 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 : ℕ
ih :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ (↑(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}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have ih₁ : ∀ (x : M),
  x ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) ↔
    x ∈ (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
Tactic: rw [Set.ext_iff] at ih
Cleared hypotheses: ih
-- 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 : ℕ
ih :
  ∀ (x : M),
    x ∈ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) ↔
      x ∈ (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
⊢ (↑(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}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have ih₁ : ∀ (x : M),
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
    Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
Tactic: simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
Cleared hypotheses: 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 : ℕ
ih :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) 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}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have succ : (↑(Submodule.span R
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M) =
  (↑(Submodule.span ℤ
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M)
Tactic: simp only [LieSubmodule.mem_top, ih, true_and]
-- 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 :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have succ : (↑(Submodule.span R
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M) ≤
  (↑(Submodule.span ℤ
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M)
Tactic: apply le_antisymm
-- 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 :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
succ :
  (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
⊢ (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have succ₁ : (↑(Submodule.span ℤ
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M) ≤
  (↑(Submodule.span R
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M)
Tactic: apply le_antisymm
-- 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 :
  ∀ (x : M),
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) x ↔
      Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) x
⊢ (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) ≤
    (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L) (n : M),
              Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
have succ : (↑(Submodule.span ℤ
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M) ≤
  (↑(Submodule.span R
        {x : M |
          ∃ (x_1 : L) (n : M),
            Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
    Set M)
Tactic: simp only [← 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 : ℕ
⊢ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
have zero : (↑(↑(lowerCentralSeries R L M 0) : Submodule R M) : Set M) = (↑(↑(lowerCentralSeries ℤ L M 0) : Submodule ℤ M) : Set M)
Tactic: induction k with
  | zero => rfl
  | succ k ih =>
    rw [lowerCentralSeries_succ, lowerCentralSeries_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [LieSubmodule.mem_top, ih, true_and]
    apply le_antisymm
    · exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
    · simp only [← ih]
      exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
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 :
  (↑(↑(lowerCentralSeries R L M 0) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M 0) : Submodule ℤ M) : Set M)
⊢ (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
have succ : ∀ (k : ℕ)
  (ih :
    (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
      (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)),
  (↑(↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M (k + 1)) : Submodule ℤ M) : Set M)
Tactic: induction k with
  | zero => rfl
  | succ k ih =>
    rw [lowerCentralSeries_succ, lowerCentralSeries_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [LieSubmodule.mem_top, ih, true_and]
    apply le_antisymm
    · exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
    · simp only [← ih]
      exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
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 : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ lcs (k + 1) N ≤ N
have succ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N) ≤ N
Tactic: simp only [lcs_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
k : ℕ
N : LieSubmodule R L M
⊢ lcs k N ≤ N
have zero : lcs 0 N ≤ N
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ]
    exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)
-- 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
zero : lcs 0 N ≤ N
⊢ lcs k N ≤ N
have succ : ∀ (k : ℕ) (ih : lcs k N ≤ N), lcs (k + 1) N ≤ N
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ]
    exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)
have succ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
  comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
Tactic: simp only [lcs_succ, lowerCentralSeries_succ] at 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_1 : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N.incl.range
have rw : lcs k N ≤ N
Tactic: rw [N.range_incl]
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
have this : lcs k N ≤ N.incl.range
Tactic: have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
-- 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
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
this : lcs k N ≤ N.incl.range
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
have succ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N)) =
  comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
Tactic: rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl 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
k_1 : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
this : lcs k N ≤ N.incl.range
succ :
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N)) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L (↥N) k) =
    comap N.incl (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N))
have succ₁ : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N)) =
  Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (comap N.incl (lcs k N))
Tactic: rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
have zero : lowerCentralSeries R L (↥N) 0 = comap N.incl (lcs 0 N)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
    have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
    rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
zero : lowerCentralSeries R L (↥N) 0 = comap N.incl (lcs 0 N)
⊢ lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
have succ : ∀ (k : ℕ) (ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)),
  lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
    have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
    rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
⊢ map N.incl (lowerCentralSeries R L (↥N) k) = lcs k N
have rw : lcs k N ≤ N
Tactic: rw [lowerCentralSeries_eq_lcs_comap, LieSubmodule.map_comap_incl, inf_eq_right]
-- 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
inst_6 : LieModule R L M
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ lcs k N = ⊥
have refine_1 : ∀ (h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥), lcs k N = ⊥
Tactic: refine ⟨fun h ↦ ?_, fun 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
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
refine_1 : ∀ (h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥), lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥ ↔ lcs k N = ⊥
have refine_2 : ∀ (h : lcs k N = ⊥), Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩