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
inst_8 : IsNoetherian R M
k : ℕ
hk : LE.le (α := LieSubmodule R L M) (genWeightSpace M 0) (LieSubmodule.ucs k ⊥)
⊢ LE.le.{u_4} (α := LieSubmodule R L M) (LieSubmodule.ucs k ⊥) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥)

Tactic:
le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k

Premises used: Set.Mem, le_iSup, Bot.bot, LieSubmodule.ucs
-- 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
k : ℕ
hk : LE.le (α := LieSubmodule R L M) (genWeightSpace M 0) (LieSubmodule.ucs k ⊥)
⊢ LE.le.{u_4} (α := LieSubmodule R L M) (LieSubmodule.ucs k ⊥) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥)

Tactic:
exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k

Premises used: le_iSup, Bot.bot, LieSubmodule.ucs
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
set :
  let φ : 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;
  ∀ {x : L} {m : M},
    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))))
        ⁅x, m⁆
⊢ ∀ {x_1 : L} {m : M},
    Membership.mem (γ := Set M)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (⨅ (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).range))))
        m →
      Membership.mem (γ := Set M)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (⨅ (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).range))))
        ⁅x_1, m⁆

Tactic:
set φ := toEnd R L M x

Premises used: LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
simp :
  ∀ (hm : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = m) (i : ℕ), ∃ (y_1 : M), (φ ^ i : (a : M) → M) y_1 = ⁅y, m⁆
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨅ (k : ℕ), (φ ^ k).range))))
    ⁅y, m⁆

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Submodule.mem_iInf, LinearMap.mem_range] at hm ⊢

Premises used: Submodule.mem_iInf, AddSubsemigroup.mem_carrier, Submodule.mem_toAddSubmonoid, LinearMap.mem_range, AddSubmonoid.mem_toSubsemigroup
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 : ℕ
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⁆
⊢ ∃ (y_1 : M), (φ ^ k : (a : M) → M) y_1 = ⁅y, m⁆

Tactic:
obtain ⟨N, hN⟩ := LieAlgebra.nilpotent_ad_of_nilpotent_algebra R L

Premises used: LieAlgebra.nilpotent_ad_of_nilpotent_algebra
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
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)
⊢ ∃ (y_1 : M), (φ ^ k : (a : M) → M) y_1 = ⁅y, m⁆

Tactic:
obtain ⟨m, rfl⟩ := hm (N + k)

Premises used: HAdd.hAdd, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 φ
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)
⊢ f₁ ^ N = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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 φ
x_1 : L
x_2 : M
⊢ Eq (α := L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₁ ^ N) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x_1 :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_2 :
      L ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x_1 : M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_2 :
      L ⊗[R] M)

Tactic:
simp [f₁, hN]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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

Tactic:
replace hN : f₁ ^ N = 0 := by ext; simp [f₁, hN]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
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)
⊢ Commute f₁ f₂

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
x_1 : L
x_2 : M
⊢ Eq (α := L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₁ * f₂) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x_1 :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_2 :
      L ⊗[R] M)
    (((((AlgebraTensorModule.curry (f₂ * f₁) : L →ₗ[R] M →ₗ[R] L ⊗[R] M) : (a : L) → M →ₗ[R] L ⊗[R] M) x_1 :
            M →ₗ[R] L ⊗[R] M) :
          (a : M) → L ⊗[R] M)
        x_2 :
      L ⊗[R] M)

Tactic:
simp [f₁, f₂]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂

Tactic:
have h₁ : Commute f₁ f₂ := by ext; simp [f₁, f₂]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂
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)
⊢ φ ∘ₗ (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) = (↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ (f₁ + f₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂
x_1 : L
x_2 : 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_1 :
            M →ₗ[R] M) :
          (a : M) → M)
        x_2 :
      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_1 :
            M →ₗ[R] M) :
          (a : M) → M)
        x_2 :
      M)

Tactic:
simp [φ, f₁, f₂]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂)

Tactic:
have h₂ : φ ∘ₗ toModuleHom R L M = toModuleHom R L M ∘ₗ (f₁ + f₂) := by ext; simp [φ, f₁, f₂]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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₂)
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)
⊢ ∃ (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

Premises used: Nat.le_succ, HAdd.hAdd, Commute.add_pow_dvd_pow_of_pow_eq_zero_right
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
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)
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ k : (a : M) → M) y_1 : M) (⁅y, (φ ^ (N + k) : (a : M) → M) m⁆ : M)

Tactic:
use toModuleHom R L M (q (y ⊗ₜ m))

Premises used: LieModule.toModuleHom, TensorProduct.tmul, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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
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)
⊢ 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:
change (φ ^ k).comp ((toModuleHom R L M : L ⊗[R] M →ₗ[R] M)) _ = _

Premises used: LieModule.toModuleHom, LieModuleHom.toLinearMap, LinearMap.comp, HPow.hPow, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
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.{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:
simp [φ, f₁, f₂, Module.End.commute_pow_left_of_commute h₂,
        LinearMap.comp_apply (g := (f₁ + f₂) ^ k), ← LinearMap.comp_apply (g := q),
        ← Module.End.mul_eq_comp, ← hq]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_apply, HPow.hPow, HAdd.hAdd, Module.End.commute_pow_left_of_commute
-- 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
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m ↔
    ∀ (k : ℕ),
      ∃ (n : 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)
                k :
              (a : M) → M)
            n =
          m

Tactic:
simp [posFittingCompOf]

Premises used: LieModule.posFittingCompOf