awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w : Weight R L M
⊢ (fun (w : (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))) ↦
        { toFun := (↑w : L → R), genWeightSpace_ne_bot' := ⋯ : Weight R L M })
      ((fun (w : Weight R L M) ↦
          (Subtype.mk (p := fun (x : L → R) ↦
              Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} x)
              w.toFun ⋯ :
            { x : L → R //
              Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} x }))
        w) =
    w

Tactic:
simp
-- 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
w : (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))
⊢ (fun (w : Weight R L M) ↦
        (Subtype.mk (p := fun (x : L → R) ↦
            Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} x)
            w.toFun ⋯ :
          { x : L → R //
            Membership.mem (γ := Set (L → R)) {χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} x }))
      ((fun (w : (↑{χ : L → R | Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥} : Type (max u_2 u_3))) ↦
          { toFun := (↑w : L → R), genWeightSpace_ne_bot' := ⋯ : Weight R L M })
        w) =
    w

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
χ : Weight R L M
x : L
⊢ Ne.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥

Tactic:
have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot
-- 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
χ : Weight R L M
x : L
this : Ne.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
contrapose :
  ∀
    (this :
      Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
        (⊥ : LieSubmodule R L M)),
    Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)

Tactic:
contrapose this
-- 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
χ : Weight R L M
x : L
this :
  Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
rw : LE.le.{u_4} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- 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
χ : Weight R L M
x : L
this :
  Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
⊢ LE.le.{u_4} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥

Tactic:
le_of_le_of_eq (iInf_le _ _) this

Premises used: le_of_le_of_eq, iInf_le
-- 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
χ : Weight R L M
x : L
this :
  Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
⊢ LE.le.{u_4} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥

Tactic:
exact le_of_le_of_eq (iInf_le _ _) this

Premises used: le_of_le_of_eq, iInf_le
-- 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
χ : Weight R L M
x : L
⊢ ∃ (x_1 : ℕ),
    ¬Eq.{u_4 + 1} (α := 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)
                  ((χ : (a : L) → R) x) :
                ℕ∞ →o Submodule R M) :
              (a : ℕ∞) → Submodule R M)
            (↑x_1 : ℕ∞) :
          Submodule R M)
        (⊥ : Submodule R M)

Tactic:
simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x

Premises used: LieModule.genWeightSpaceOf, Module.End.iSup_genEigenspace_eq, LieModule.Weight.genWeightSpaceOf_ne_bot
-- 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
χ : Weight R L M
x : L
obtain :
  ∀ (k : ℕ)
    (hk :
      Ne.{u_4 + 1} (α := 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)
                  ((χ : (a : L) → R) x) :
                ℕ∞ →o Submodule R M) :
              (a : ℕ∞) → Submodule R M)
            (↑k : ℕ∞) :
          Submodule R M)
        (⊥ : Submodule R M)),
    Module.End.HasEigenvalue.{u_2, u_4} (R := R) (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 : Module.End R M)
      ((χ : (a : L) → R) x : R)
⊢ Module.End.HasEigenvalue.{u_2, u_4} (R := R) (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 : Module.End R M)
    ((χ : (a : L) → R) x : R)

Tactic:
obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by
    simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x
-- 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
χ : Weight R L M
x : L
k : ℕ
hk :
  Ne.{u_4 + 1} (α := 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)
              ((χ : (a : L) → R) x) :
            ℕ∞ →o Submodule R M) :
          (a : ℕ∞) → Submodule R M)
        (↑k : ℕ∞) :
      Submodule R M)
    (⊥ : Submodule R M)
⊢ Module.End.HasEigenvalue.{u_2, u_4} (R := R) (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 : Module.End R M)
    ((χ : (a : L) → R) x : R)

Tactic:
Module.End.hasEigenvalue_of_hasGenEigenvalue hk

Premises used: Module.End.hasEigenvalue_of_hasGenEigenvalue
-- 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
χ : Weight R L M
x : L
k : ℕ
hk :
  Ne.{u_4 + 1} (α := 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)
              ((χ : (a : L) → R) x) :
            ℕ∞ →o Submodule R M) :
          (a : ℕ∞) → Submodule R M)
        (↑k : ℕ∞) :
      Submodule R M)
    (⊥ : Submodule R M)
⊢ Module.End.HasEigenvalue.{u_2, u_4} (R := R) (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 : Module.End R M)
    ((χ : (a : L) → R) x : R)

Tactic:
exact Module.End.hasEigenvalue_of_hasGenEigenvalue hk

Premises used: Module.End.hasEigenvalue_of_hasGenEigenvalue
-- 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 : IsDomain R
inst_9 : Module.IsTorsionFree R M
inst_10 : IsReduced R
x : L
h :
  _root_.IsNilpotent.{u_4} (R := 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)
χ : Weight R L M
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)

Tactic:
((χ.hasEigenvalueAt x).isNilpotent_of_isNilpotent h).eq_zero

Premises used: Module.End.HasEigenvalue.isNilpotent_of_isNilpotent, IsNilpotent.eq_zero, LieModule.Weight.hasEigenvalueAt
-- 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
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M 0) ⊤

Tactic:
simp [genWeightSpace, genWeightSpaceOf]

Premises used: LieModule.genWeightSpaceOf, LieModule.genWeightSpace
-- 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
χ : L → R
h :
  ∀ (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
⊢ Eq (α := Submodule R M) (↑(genWeightSpace M (χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))) : Submodule R M)
    (↑(genWeightSpace M χ) : Submodule R M)

Tactic:
ext m
-- 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
χ : L → R
m : M
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)
⊢ 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

Tactic:
simp only [mem_genWeightSpace, LieSubmodule.mem_toSubmodule, Subtype.forall]

Premises used: LieSubmodule.mem_toSubmodule, LieModule.mem_genWeightSpace, Subtype.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
χ : L → R
m : M
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)
⊢ (∀ (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:
apply forall_congr'

Premises used: forall_congr'
-- 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
χ : 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)) ↔
      ∃ (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:
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
inst_8 : IsNilpotent L M
⊢ Eq (α := LieSubmodule.{u_2, u_3, u_4} R (↥⊤) M) (genWeightSpace M 0) ⊤

Tactic:
simp_all
-- 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
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))
⊢ ∃ (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)

Tactic:
use (toEnd R L M x).maxGenEigenspaceIndex (χ x)

Premises used: Module.End.maxGenEigenspaceIndex, LieModule.toEnd, 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
χ : L → R
x : L
m : M
hm : Membership.mem (γ := Submodule R M) (↑(genWeightSpace M χ) : Submodule R M) m
⊢ 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
-- 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
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))
h₁ h₂ h₃ 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))
⊢ 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

Premises used: Module.End.maxGenEigenspace_eq, Module.End.genEigenspace_nat
-- 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
⊢ ∃ (k : ℕ),
    (↑(genWeightSpace M 0) : Submodule R M) ≤
      LinearMap.ker
        (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)

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

Premises used: LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, OfNat.ofNat