awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
m : M
hm :
  ∀ (x x_1 : L),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x_1 :
                  Module.End R M)
                k :
              (a : M) → M)
            ⁅x, m⁆ :
          M)
        (0 : M)
y : L
k : ℕ
hk :
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
              Module.End R M)
            k :
          (a : M) → M)
        ⁅y, m⁆ :
      M)
    (0 : M)
⊢ ∃ (k : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)
have h : Eq (α := M)
  ((HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
          (k + 1) :
        (a : M) → M)
      m :
    M)
  (0 : M)
Tactic: use k + 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
⊢ Eq (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)
have obtain : ∀ (k : ℕ) (hk : LE.le (α := LieSubmodule R L M) (genWeightSpace M 0) (LieSubmodule.ucs k ⊥)),
  Eq (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)
Tactic: obtain ⟨k, hk⟩ := (LieSubmodule.isNilpotent_iff_exists_self_le_ucs
    <| genWeightSpace M (0 : L → R)).mp inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
inst_8 : IsNoetherian R M
k : ℕ
hk : LE.le (α := LieSubmodule R L M) (genWeightSpace M 0) (LieSubmodule.ucs k ⊥)
⊢ Eq (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)
have refine : LE.le.{u_4} (α := LieSubmodule R L M) (LieSubmodule.ucs k ⊥) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥)
Tactic: refine le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
m : M
hm :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨅ (k : ℕ), (φ ^ k).range))))
    m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨅ (k : ℕ), (φ ^ k).range))))
    ⁅y, m⁆
have simp : ∀ (hm : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = m) (i : ℕ), ∃ (y_1 : M), (φ ^ i : (a : M) → M) y_1 = ⁅y, m⁆
Tactic: simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Submodule.mem_iInf, LinearMap.mem_range] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
m : M
hm : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = m
k : ℕ
⊢ ∃ (y_1 : M), (φ ^ k : (a : M) → M) y_1 = ⁅y, m⁆
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ (x : L),
      HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) x : Module.End R L) N = 0),
  ∃ (y_1 : M), (φ ^ k : (a : M) → M) y_1 = ⁅y, m⁆
Tactic: obtain ⟨N, hN⟩ := LieAlgebra.nilpotent_ad_of_nilpotent_algebra R L
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
m : M
hm : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = m
k N : ℕ
hN :
  ∀ (x : L), HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) x : Module.End R L) N = 0
⊢ ∃ (y_1 : M), (φ ^ k : (a : M) → M) y_1 = ⁅y, m⁆
have obtain : ∀ (m : M) (hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)),
  ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
Tactic: obtain ⟨m, rfl⟩ := hm (N + k)
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
hN :
  ∀ (x : L), HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) x : Module.End R L) N = 0
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
⊢ f₁ ^ N = 0
have a : ∀ (x : L) (x_1 : M),
  Eq (α := L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₁ ^ N) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_1 :
      L ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x : M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_1 :
      L ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
hN :
  ∀ (x : L), HPow.hPow (α := Module.End R L) ((LieAlgebra.ad R L : (a : L) → Module.End R L) x : Module.End R L) N = 0
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have hN₁ : f₁ ^ N = 0
Tactic: replace hN : f₁ ^ N = 0 := by ext; simp [f₁, hN]
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
⊢ Commute f₁ f₂
have a : ∀ (x : L) (x_1 : M),
  Eq (α := L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₁ * f₂) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_1 :
      L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₂ * f₁) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_1 :
      L ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have h₁ : Commute f₁ f₂
Tactic: have h₁ : Commute f₁ f₂ := by ext; simp [f₁, f₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
⊢ φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)
have a : ∀ (x : L) (x_1 : M),
  Eq (α := M)
    (((((AlgebraTensorModule.curry (φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (M →ₗ[R] M)) :
                (a : L) → M →ₗ[R] M)
              x :
            M →ₗ[R] M) :
          (a : M) → M)
        x_1 :
      M)
    (((((AlgebraTensorModule.curry ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (M →ₗ[R] M)) :
                (a : L) → M →ₗ[R] M)
              x :
            M →ₗ[R] M) :
          (a : M) → M)
        x_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have h₂ : φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)
Tactic: have h₂ : φ ∘ₗ toModuleHom R L M = toModuleHom R L M ∘ₗ (f₁ + f₂) := by ext; simp [φ, f₁, f₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have obtain : ∀ (q : Module.End R (L ⊗[R] M)) (hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q),
  ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
Tactic: obtain ⟨q, hq⟩ := h₁.add_pow_dvd_pow_of_pow_eq_zero_right (N + k).le_succ hN
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have h : Eq (α := M)
  ((φ ^ k : (a : M) → M)
      ((toModuleHom R L M : (a : L ⊗[R] M) → M) ((q : (a : L ⊗[R] M) → L ⊗[R] M) (y ⊗ₜ[R] m) : L ⊗[R] M) : M) :
    M)
  (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
Tactic: use toModuleHom R L M (q (y ⊗ₜ m))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ ^ (N + k) : (a : M) → M) m : M)
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ Eq (α := M)
    ((φ ^ k : (a : M) → M)
        ((toModuleHom R L M : (a : L ⊗[R] M) → M) ((q : (a : L ⊗[R] M) → L ⊗[R] M) (y ⊗ₜ[R] m) : L ⊗[R] M) : M) :
      M)
    (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
have h : Eq.{u_4 + 1} (α := M)
  (((φ ^ k) ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      ((q : (a : L ⊗[R] M) → L ⊗[R] M) (y ⊗ₜ[R] m) : L ⊗[R] M) :
    M)
  (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)
Tactic: change (φ ^ k).comp ((toModuleHom R L M : L ⊗[R] M →ₗ[R] M)) _ = _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
k : ℕ
this :
  ∀ (m : M) (l : ℕ),
    Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              l :
            (a : M) → M)
          m :
        M)
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m
have obtain : ∀ (n : M)
  (hm :
    Membership.mem (α := M) (γ := LieSubmodule R L M) (posFittingCompOf R M x)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              k :
            (a : M) → M)
          n :
        M)),
  Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            k :
          (a : M) → M)
        n :
      M)
Tactic: obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
k : ℕ
⊢ LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (lowerCentralSeries R L M k)
have suffices : ∀ (m : M) (l : ℕ),
  Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            l :
          (a : M) → M)
        m :
      M)
Tactic: suffices ∀ m l, (toEnd R L M x ^ l) m ∈ lowerCentralSeries R L M l by
    intro m hm
    obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
    exact this n k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
ih :
  Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            l :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M (l + 1))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            (l + 1) :
          (a : M) → M)
        m :
      M)
have succ : Membership.mem (α := M) (γ := LieSubmodule R L M)
  (Bracket.bracket.{u_3, u_4} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M l))
  (((((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              l :
            (a : M) → M)
          m :
        M) :
    M)
Tactic: simp only [lowerCentralSeries_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
⊢ Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            l :
          (a : M) → M)
        m :
      M)
have zero : Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M 0)
  ((HPow.hPow (α := Module.End R M) (β := ℕ)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
          0 :
        (a : M) → M)
      m :
    M)
Tactic: induction l with
  | zero => simp
  | succ l ih =>
    simp only [lowerCentralSeries_succ, pow_succ', Module.End.mul_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
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 : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
zero :
  Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M 0)
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            0 :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            l :
          (a : M) → M)
        m :
      M)
have succ : ∀ (l : ℕ)
  (ih :
    Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M l)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              l :
            (a : M) → M)
          m :
        M)),
  Membership.mem (α := M) (γ := LieSubmodule R L M) (lowerCentralSeries R L M (l + 1))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            (l + 1) :
          (a : M) → M)
        m :
      M)
Tactic: induction l with
  | zero => simp
  | succ l ih =>
    simp only [lowerCentralSeries_succ, pow_succ', Module.End.mul_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih
Cleared hypotheses: l