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
χ : L → R
m : M
⊢ Membership.mem (γ := Submodule R M)
      (↑(genWeightSpace M (χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))) : Submodule R M) m ↔
    Membership.mem (γ := Submodule R M) (↑(genWeightSpace M χ) : Submodule R M) m
have h : (∀ (a : L) (b : Membership.mem (γ := LieSubalgebra R L) ⊤ a),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HSub.hSub (α := Module.End R M)
                  ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M)
                      (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b) :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M)
                    ((χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))
                      (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b))
                    1) ^
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)) ↔
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HSub.hSub (α := 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)
                  (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)
Tactic: simp only [mem_genWeightSpace, LieSubmodule.mem_toSubmodule, Subtype.forall]
-- 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
χ : L → R
m : M
⊢ (∀ (a : L) (b : Membership.mem (γ := LieSubalgebra R L) ⊤ a),
      ∃ (k : ℕ),
        Eq (α := M)
          ((HSub.hSub (α := Module.End R M)
                    ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M)
                        (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b) :
                      Module.End R M)
                    (HSMul.hSMul (β := Module.End R M)
                      ((χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))
                        (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b))
                      1) ^
                  k :
                (a : M) → M)
              m :
            M)
          (0 : M)) ↔
    ∀ (x : L),
      ∃ (k : ℕ),
        Eq (α := M)
          ((HSub.hSub (α := 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)
                    (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
                  k :
                (a : M) → M)
              m :
            M)
          (0 : M)
have h : ∀ (a : L),
  (∀ (b : Membership.mem (γ := LieSubalgebra R L) ⊤ a),
      ∃ (k : ℕ),
        Eq (α := M)
          ((HSub.hSub (α := Module.End R M)
                    ((toEnd R (↥⊤) M : (a : ↥⊤) → Module.End R M)
                        (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b) :
                      Module.End R M)
                    (HSMul.hSMul (β := Module.End R M)
                      ((χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))
                        (Subtype.mk (p := fun (a : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊤ a) a b))
                      1) ^
                  k :
                (a : M) → M)
              m :
            M)
          (0 : M)) ↔
    ∃ (k : ℕ),
      Eq (α := M)
        ((HSub.hSub (α := 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) a :
                    Module.End R M)
                  (HSMul.hSMul (β := Module.End R M) (χ a) 1) ^
                k :
              (a : M) → M)
            m :
          M)
        (0 : M)
Tactic: apply forall_congr'
-- 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
χ : L → R
x : L
⊢ ∃ (k : ℕ),
    (↑(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)
have h : (↑(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) ^
      Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
Tactic: use (toEnd R L M x).maxGenEigenspaceIndex (χ x)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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
m : M
hm : Membership.mem (γ := Submodule R M) (↑(genWeightSpace M χ) : Submodule R M) m
⊢ 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) ^
        Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
have hm₁ : Membership.mem (γ := Submodule R M)
  (Module.End.maxGenEigenspace
    (((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))
  m
Tactic: replace hm : m ∈ (toEnd R L M x).maxGenEigenspace (χ x) :=
    genWeightSpace_le_genWeightSpaceOf M x χ hm
Cleared hypotheses: 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
inst_8 : IsNoetherian R M
χ : L → R
x : L
m : M
hm :
  Membership.mem (γ := Submodule R M)
    (Module.End.maxGenEigenspace
      (((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))
    m
⊢ 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) ^
        Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
have h : ∀
  (hm :
    Membership.mem (γ := Submodule R M)
      ((Module.End.genEigenspace
              (((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) :
            (a : ℕ∞) → Submodule R M)
          (↑(Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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)) :
            ℕ∞) :
        Submodule R M)
      m),
  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) ^
        Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
Tactic: rwa [Module.End.maxGenEigenspace_eq, Module.End.genEigenspace_nat] at hm
Cleared hypotheses: 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
inst_8 : IsNoetherian R M
χ : L → R
x : L
m : M
hm :
  Membership.mem (γ := Submodule R M)
    (Module.End.maxGenEigenspace
      (((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))
    m
h :
  ∀
    (hm :
      Membership.mem (γ := Submodule R M)
        ((Module.End.genEigenspace
                (((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) :
              (a : ℕ∞) → Submodule R M)
            (↑(Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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)) :
              ℕ∞) :
          Submodule R M)
        m),
    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) ^
          Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
⊢ 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) ^
        Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
have h₁ : ∀
  (hm :
    m ∈
      (HSub.hSub (α := 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)
            (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
          Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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)).ker),
  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) ^
        Module.End.maxGenEigenspaceIndex.{u_2, u_4} (M := 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))
Tactic: rwa [Module.End.maxGenEigenspace_eq, Module.End.genEigenspace_nat] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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
⊢ _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 χ)))
have 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))
    sorry
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
-- 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
χ : 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))
      ⋯
⊢ _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 χ)))
have 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 χ)))
Tactic: obtain ⟨k, hk⟩ := exists_genWeightSpace_le_ker_of_isNoetherian M χ x
-- 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
χ : 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)
⊢ _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 χ)))
have 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
Tactic: use 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
⊢ Eq (α := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) (genWeightSpace M 0)
have refine : LE.le (α := LieSubmodule R L M) (LieSubmodule.normalizer (genWeightSpace M 0)) (genWeightSpace M 0)
Tactic: refine le_antisymm ?_ (LieSubmodule.le_normalizer _)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
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
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m
have hm₁ : ∀ (x : L), Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) ⁅x, m⁆
Tactic: rw [LieSubmodule.mem_normalizer] at hm
Cleared hypotheses: 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
m : M
hm : ∀ (x : L), Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) ⁅x, m⁆
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m
have 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)
Tactic: simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm ⊢
Cleared hypotheses: 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
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 : ℕ),
    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 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)
Tactic: obtain ⟨k, hk⟩ := hm y y