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
χ : L → R
x : L
⊢ HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R 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
inst_8 : IsNoetherian R M
χ : L → R
x : L
⊢ HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯

Tactic:
have : toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x) =
      (toEnd R L M x - algebraMap R _ (χ x)).restrict
        (fun m hm ↦ sub_mem (LieSubmodule.lie_mem _ hm) (Submodule.smul_mem _ _ hm)) := by
    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
inst_8 : IsNoetherian R M
χ : L → R
x : L
this :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯
obtain :
  ∀ (k : ℕ)
    (hk :
      (↑(genWeightSpace M χ) : Submodule R M) ≤
        LinearMap.ker
          (HSub.hSub (α := Module.End R M) (β := 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)
              ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
            k)),
    _root_.IsNilpotent
      (HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
        (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
              (a : L) → Module.End R ↥(genWeightSpace M χ))
            x :
          Module.End R ↥(genWeightSpace M χ))
        ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
          Module.End R ↥(genWeightSpace M χ)))
⊢ _root_.IsNilpotent
    (HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)))

Tactic:
obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x

Premises used: LieModule.exists_genWeightSpace_le_ker_of_isNoetherian
-- 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
χ : L → R
x : L
this :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯
k : ℕ
hk :
  (↑(genWeightSpace M χ) : Submodule R M) ≤
    LinearMap.ker
      (HSub.hSub (α := Module.End R M) (β := 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)
          ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
        k)
h :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
        (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
              (a : L) → Module.End R ↥(genWeightSpace M χ))
            x :
          Module.End R ↥(genWeightSpace M χ))
        ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
          Module.End R ↥(genWeightSpace M χ)) ^
      k =
    0
⊢ _root_.IsNilpotent
    (HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace 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
χ : L → R
x : L
this :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯
k : ℕ
hk :
  (↑(genWeightSpace M χ) : Submodule R M) ≤
    LinearMap.ker
      (HSub.hSub (α := Module.End R M) (β := 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)
          ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
        k)
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
⊢ Eq (α := ↥(genWeightSpace M χ))
    (((HSub.hSub (α := Module.End R M) (β := 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)
                  ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
                k).restrict
            ⋯ :
          (a : ↥(genWeightSpace M χ)) → ↥(genWeightSpace M χ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) x) m hm) :
      ↥(genWeightSpace M χ))
    (0 : ↥(genWeightSpace M χ))

Tactic:
ZeroMemClass.coe_eq_zero.mp (hk hm)

Premises used: ZeroMemClass.coe_eq_zero, Iff.mp
-- 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
χ : L → R
x : L
this :
  HSub.hSub (α := Module.End R ↥(genWeightSpace M χ)) (β := Module.End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
              LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M χ))) :
            (a : L) → Module.End R ↥(genWeightSpace M χ))
          x :
        Module.End R ↥(genWeightSpace M χ))
      ((algebraMap R (Module.End R ↥(genWeightSpace M χ)) : (a : R) → Module.End R ↥(genWeightSpace M χ)) (χ x) :
        Module.End R ↥(genWeightSpace M χ)) =
    LinearMap.restrict
      (HSub.hSub (α := Module.End R M) (β := 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)
        ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M))
      ⋯
k : ℕ
hk :
  (↑(genWeightSpace M χ) : Submodule R M) ≤
    LinearMap.ker
      (HSub.hSub (α := Module.End R M) (β := 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)
          ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
        k)
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
⊢ Eq (α := ↥(genWeightSpace M χ))
    (((HSub.hSub (α := Module.End R M) (β := 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)
                  ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) (χ x) : Module.End R M) ^
                k).restrict
            ⋯ :
          (a : ↥(genWeightSpace M χ)) → ↥(genWeightSpace M χ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) x) m hm) :
      ↥(genWeightSpace M χ))
    (0 : ↥(genWeightSpace M χ))

Tactic:
exact ZeroMemClass.coe_eq_zero.mp (hk hm)
-- 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
x : L
⊢ _root_.IsNilpotent.{u_4} (R := Module.End R ↥(genWeightSpace M 0))
    (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M 0) :
            LieHom.{u_2, u_3, u_4} R L (Module.End R ↥(genWeightSpace M 0))) :
          (a : L) → Module.End R ↥(genWeightSpace M 0))
        x :
      Module.End R ↥(genWeightSpace M 0))

Tactic:
simpa using isNilpotent_toEnd_sub_algebraMap M (0 : L → R) x

Premises used: LieModule.isNilpotent_toEnd_sub_algebraMap, OfNat.ofNat
-- 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
inst_8 : IsNoetherian R M
⊢ IsNilpotent.{u_3, u_4} L ↥(genWeightSpace M 0)

Tactic:
isNilpotent_iff_forall'.mpr <| isNilpotent_toEnd_genWeightSpace_zero M

Premises used: Iff.mpr, LieModule.isNilpotent_toEnd_genWeightSpace_zero, 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
⊢ Eq (α := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) (genWeightSpace M 0)

Tactic:
le_antisymm ?_ (LieSubmodule.le_normalizer _)

Premises used: le_antisymm, LieSubmodule.le_normalizer
-- 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
refine : LE.le (α := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) (genWeightSpace M 0)
⊢ Eq (α := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) (genWeightSpace M 0)

Tactic:
refine le_antisymm ?_ (LieSubmodule.le_normalizer _)

Premises used: le_antisymm, LieSubmodule.le_normalizer
-- 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
hm : Membership.mem (γ := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) m
⊢ ∀ (x : L), Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) ⁅x, m⁆

Tactic:
rw [LieSubmodule.mem_normalizer] at hm

Premises used: LieSubmodule.mem_normalizer
-- 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
hm : ∀ (x : L), Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) ⁅x, m⁆
simp :
  ∀
    (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))
    (x : 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 :
                  Module.End R M)
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm ⊢

Premises used: sub_zero, LieModule.mem_genWeightSpace, Pi.zero_apply, zero_smul
-- 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
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
obtain :
  ∀ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨k, hk⟩ := hm y y
-- 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
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)
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)
⊢ ∃ (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)

Tactic:
use k + 1
-- 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
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)
⊢ 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:
simpa [pow_succ, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, 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
⊢ LE.le (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)

Tactic:
simpa using
    LieSubmodule.ucs_le_of_normalizer_eq_self (genWeightSpace_zero_normalizer_eq_self R L M)

Premises used: LieModule.genWeightSpace_zero_normalizer_eq_self, LieSubmodule.ucs_le_of_normalizer_eq_self
-- 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
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)
⊢ 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

Premises used: LieSubmodule.isNilpotent_iff_exists_self_le_ucs, inferInstance, Iff.mp, LieModule.genWeightSpace, OfNat.ofNat
-- 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 ⊥)
⊢ Eq (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)

Tactic:
le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)

Premises used: LieModule.iSup_ucs_le_genWeightSpace_zero, le_antisymm, le_trans
-- 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 ⊥)
refine : LE.le.{u_4} (α := LieSubmodule R L M) (LieSubmodule.ucs k ⊥) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥)
⊢ Eq (α := LieSubmodule R L M) (⨆ (k : ℕ), LieSubmodule.ucs k ⊥) (genWeightSpace M 0)

Tactic:
refine le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)

Premises used: LieModule.iSup_ucs_le_genWeightSpace_zero, le_antisymm, le_trans