awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
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)
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) m

Tactic:
obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k

Premises used: LieModule.mem_posFittingCompOf, Iff.mp, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
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:
this n k
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
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:
exact this n k
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 : ℕ
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)
⊢ LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (lowerCentralSeries R L M k)

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
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
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)
⊢ 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:
simp only [lowerCentralSeries_succ, pow_succ', Module.End.mul_apply]

Premises used: LieModule.lowerCentralSeries_succ, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
    (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:
LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Premises used: Set.Mem, LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
    (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:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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)
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)
⊢ 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:
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

Premises used: LieModule.lowerCentralSeries_succ, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 : IsNilpotent L M
x : L
simp_rw : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥
simp_rw₁ : LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨅ (k : ℕ), lowerCentralSeries R L M k)
simp_rw₂ : ∀ (i : ℕ), LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (lowerCentralSeries R L M i)
simp_rw₃ : ∀ (i : ℕ), True
⊢ Eq (α := LieSubmodule R L M) (posFittingCompOf R M x) ⊥

Tactic:
simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
    posFittingCompOf_le_lowerCentralSeries, forall_const]

Premises used: le_iInf_iff, LieModule.posFittingCompOf_le_lowerCentralSeries, forall_const, eq_bot_iff, LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m ↔
    Membership.mem (γ := LieSubmodule R L M) (⨆ (x : L), posFittingCompOf R M x) m

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨆ (x : L), posFittingCompOf R M x)

Tactic:
le_iSup (posFittingCompOf R M) x

Premises used: Set.Mem, setOf, le_iSup, LieModule.posFittingCompOf
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ LE.le (α := LieSubmodule R L M) (posFittingCompOf R M x) (⨆ (x : L), posFittingCompOf R M x)

Tactic:
exact le_iSup (posFittingCompOf R M) x

Premises used: le_iSup, LieModule.posFittingCompOf
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
⊢ LE.le (α := LieSubmodule R L M) (posFittingComp R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k)

Tactic:
simp [posFittingComp]

Premises used: LieModule.posFittingComp
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
⊢ Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)

Tactic:
le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)

Premises used: LieModule.posFittingComp_le_iInf_lowerCentralSeries, le_antisymm
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
refine : LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)
⊢ Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)

Tactic:
refine le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)

Premises used: LieModule.posFittingComp_le_iInf_lowerCentralSeries, le_antisymm
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
h : IsNilpotent.{u_3, u_4} L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
⊢ LE.le (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (posFittingComp R L M)

Tactic:
apply iInf_lcs_le_of_isNilpotent_quot

Premises used: LieModule.iInf_lcs_le_of_isNilpotent_quot
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
h :
  ∀ (x : L),
    _root_.IsNilpotent.{u_4} (R :=
      Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
            (a : L) → Module.End R (M ⧸ posFittingComp R L M))
          x :
        Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
⊢ IsNilpotent.{u_3, u_4} L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))

Tactic:
rw [LieModule.isNilpotent_iff_forall' (R := R)]

Premises used: LieModule.isNilpotent_iff_forall'
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
x : L
h :
  ∀ (k : ℕ)
    (hk :
      ∀ b ≥ k,
        ⨅ (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)
                m).range =
          (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)
              b).range),
    _root_.IsNilpotent.{u_4} (R :=
      Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
            (a : L) → Module.End R (M ⧸ posFittingComp R L M))
          x :
        Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
⊢ _root_.IsNilpotent.{u_4} (R := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
    ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
          (a : L) → Module.End R (M ⧸ posFittingComp R L M))
        x :
      Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))

Tactic:
obtain ⟨k, hk⟩ := Filter.eventually_atTop.mp (toEnd R L M x).eventually_iInf_range_pow_eq

Premises used: LinearMap.eventually_iInf_range_pow_eq, Iff.mp, LieModule.toEnd, Filter.eventually_atTop, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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)
            m).range =
      (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)
          b).range
h :
  HPow.hPow (α := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
            (a : L) → Module.End R (M ⧸ posFittingComp R L M))
          x :
        Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      k =
    0
⊢ _root_.IsNilpotent.{u_4} (R := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
    ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
          (a : L) → Module.End R (M ⧸ posFittingComp R L M))
        x :
      Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
inst_9 : IsArtinian R M
x : L
k : ℕ
hk :
  ∀ b ≥ k,
    ⨅ (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)
            m).range =
      (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)
          b).range
h :
  ∀ (x_1 : HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) (m : M),
    Eq (α := HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
      ((HPow.hPow (α := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
              ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
                    (a : L) → Module.End R (M ⧸ posFittingComp R L M))
                  x :
                Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
              k :
            (a : M ⧸ posFittingComp R L M) → M ⧸ posFittingComp R L M)
          (Quot.mk (⇑(↑(posFittingComp R L M) : Submodule R M).quotientRel : M → M → Prop) m) :
        HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
      ((0 : (a : M ⧸ posFittingComp R L M) → M ⧸ posFittingComp R L M)
          (Quot.mk (⇑(↑(posFittingComp R L M) : Submodule R M).quotientRel : M → M → Prop) m) :
        HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M))
⊢ HPow.hPow (α := Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      ((toEnd R L (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)) :
            (a : L) → Module.End R (M ⧸ posFittingComp R L M))
          x :
        Module.End R (HasQuotient.Quotient M (B := LieSubmodule R L M) (posFittingComp R L M)))
      k =
    0

Tactic:
ext ⟨m⟩