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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
this :
  ∃ (φ : R),
    Ne.{u_4 + 1} (α := 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) φ)
      ⊥
obtain :
  ∀ (φ : R)
    (hφ :
      Ne.{u_4 + 1} (α := 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) φ)
        ⊥),
    ∃ (φ : R),
      Module.End.HasEigenvalue.{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) φ
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{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) φ

Tactic:
obtain ⟨φ, hφ⟩ := 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
φ : R
hφ :
  Ne.{u_4 + 1} (α := 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) φ)
    ⊥
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{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) φ

Tactic:
⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩

Premises used: ENat.top_pos, Exists.intro, Iff.mp, Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one
-- 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
φ : R
hφ :
  Ne.{u_4 + 1} (α := 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) φ)
    ⊥
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{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) φ

Tactic:
exact ⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩
-- 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
suffices :
  ∃ (φ : R),
    Ne.{u_4 + 1} (α := 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) φ)
      ⊥
⊢ ∃ (φ : R),
    Module.End.HasEigenvalue.{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) φ

Tactic:
suffices ∃ φ, (toEnd R L M x).maxGenEigenspace φ ≠ ⊥ by
    obtain ⟨φ, hφ⟩ := this
    exact ⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩
-- 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      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) φ)
    ⊤

Tactic:
have := maxGenEigenspace_eq_top (R := R) (L := L) (M := M) 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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
this :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      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) φ)
    ⊤
contrapose! :
  ∀
    (this :
      ∀ (φ : R),
        Eq.{u_4 + 1} (α := 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) φ)
          ⊥),
    Ne.{u_4 + 1} (α := Submodule R M)
      (⨆ (φ : R),
        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) φ)
      ⊤
⊢ ∃ (φ : R),
    Ne.{u_4 + 1} (α := 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) φ)
      ⊥

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 : Nontrivial M
inst_8 : IsTriangularizable R L M
x : L
this :
  ∀ (φ : R),
    Eq.{u_4 + 1} (α := 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) φ)
      ⊥
⊢ Ne.{u_4 + 1} (α := Submodule R M)
    (⨆ (φ : R),
      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) φ)
    ⊤

Tactic:
simp [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
inst_8 : IsTriangularizable R L M
x : L
rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : R), (↑(genWeightSpaceOf M i x) : Submodule R M)) ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨆ (φ : R), genWeightSpaceOf M φ x) ⊤

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
    LieSubmodule.top_toSubmodule]

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj
-- 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 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (i : R),
      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) i)
    ⊤

Tactic:
IsTriangularizable.maxGenEigenspace_eq_top x

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsTriangularizable R L M
x : L
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨆ (i : R),
      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) i)
    ⊤

Tactic:
exact IsTriangularizable.maxGenEigenspace_eq_top x

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
this :
  _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        (HSub.hSub (α := End R ↥(genWeightSpace M χ))
          (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) :
                  LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
                (a : L) → End R ↥(genWeightSpace M χ))
              x :
            End R ↥(genWeightSpace M χ))
          (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id)) :
      R)
    (0 : R)

Tactic:
replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
-- 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 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
suffices :
  _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))
⊢ (trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ)) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x

Tactic:
suffices _root_.IsNilpotent ((toEnd R L (genWeightSpace M χ) x) - χ x • LinearMap.id) by
    replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
    rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
      ← nsmul_eq_mul] at 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
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
rw :
  _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      ((algebraMap R (End R ↥(genWeightSpace M χ)) : (a : R) → End R ↥(genWeightSpace M χ)) (χ x) :
        End R ↥(genWeightSpace M χ)))
⊢ _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      (HSMul.hSMul (β := ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) (χ x) LinearMap.id))

Tactic:
rw [← Module.algebraMap_end_eq_smul_id]

Premises used: Module.algebraMap_end_eq_smul_id
-- 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 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
⊢ _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      ((algebraMap R (End R ↥(genWeightSpace M χ)) : (a : R) → End R ↥(genWeightSpace M χ)) (χ x) :
        End R ↥(genWeightSpace M χ)))

Tactic:
isNilpotent_toEnd_sub_algebraMap M χ x

Premises used: LieModule.isNilpotent_toEnd_sub_algebraMap
-- 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 : IsPrincipalIdealRing R
inst_10 : Free R M
inst_11 : Module.Finite R M
χ : L → R
x : L
⊢ _root_.IsNilpotent
    (HSub.hSub (α := End R ↥(genWeightSpace M χ)) (β := End R ↥(genWeightSpace M χ))
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          x :
        End R ↥(genWeightSpace M χ))
      ((algebraMap R (End R ↥(genWeightSpace M χ)) : (a : R) → End R ↥(genWeightSpace M χ)) (χ x) :
        End R ↥(genWeightSpace M χ)))

Tactic:
exact isNilpotent_toEnd_sub_algebraMap M χ x

Premises used: LieModule.isNilpotent_toEnd_sub_algebraMap
-- 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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
inst_13 : IsAlgClosed K
⊢ IsTriangularizable K L M

Tactic:
⟨fun _ ↦ Module.End.iSup_maxGenEigenspace_eq_top _⟩

Premises used: LieModule.IsTriangularizable.mk, LieModule.toEnd, Module.End.iSup_maxGenEigenspace_eq_top, 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
inst_8 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
⊢ IsTriangularizable.{u_1, u_3, u_4} K L ↥N

Tactic:
⟨fun y ↦ ?_⟩

Premises used: LieModule.IsTriangularizable.mk
-- 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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
refine :
  ∀ (y : L),
    Eq.{u_4 + 1} (α := Submodule K ↥N)
      (⨆ (φ : K),
        End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
          (((toEnd.{u_1, u_3, u_4} K L ↥N : LieHom.{u_1, u_3, u_4} K L (End K ↥N)) : (a : L) → End K ↥N) y) φ)
      ⊤
⊢ IsTriangularizable.{u_1, u_3, u_4} K L ↥N

Tactic:
refine ⟨fun y ↦ ?_⟩
-- 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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
y : L
rw :
  Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (LinearMap.restrict (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) ⋯) φ)
    ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (((toEnd.{u_1, u_3, u_4} K L ↥N : LieHom.{u_1, u_3, u_4} K L (End K ↥N)) : (a : L) → End K ↥N) y) φ)
    ⊤

Tactic:
rw [← N.toEnd_restrict_eq_toEnd y]

Premises used: LieSubmodule.toEnd_comp_subtype_mem, LieSubmodule.toEnd_restrict_eq_toEnd
-- 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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
y : L
⊢ Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (LinearMap.restrict (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) ⋯) φ)
    ⊤

Tactic:
Module.End.genEigenspace_restrict_eq_top _ (IsTriangularizable.maxGenEigenspace_eq_top y)

Premises used: Set.Mem, setOf, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Module.End.genEigenspace_restrict_eq_top
-- 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 : Field K
inst_9 : LieAlgebra K L
inst_10 : Module K M
inst_11 : LieModule K L M
inst_12 : FiniteDimensional K M
N : LieSubmodule K L M
inst_13 : IsTriangularizable K L M
y : L
⊢ Eq.{u_4 + 1} (α := Submodule K ↥N)
    (⨆ (φ : K),
      End.maxGenEigenspace.{u_1, u_4} (M := ↥N)
        (LinearMap.restrict (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) ⋯) φ)
    ⊤

Tactic:
exact Module.End.genEigenspace_restrict_eq_top _ (IsTriangularizable.maxGenEigenspace_eq_top y)

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Module.End.genEigenspace_restrict_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
simp :
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (i : L → K), ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule K M)) ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤

Tactic:
simp only [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
    LieSubmodule.iInf_toSubmodule, LieSubmodule.top_toSubmodule, genWeightSpace]

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.iInf_toSubmodule, LieSubmodule.toSubmodule_inj, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (i : L → K), ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule K M)) ⊤

Tactic:
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_

Premises used: LieModule.genWeightSpaceOf, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, LieSubmodule.lie_mem, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
refine :
  ∀ (i : L),
    Eq.{u_4 + 1} (α := Submodule K M)
      (⨆ (μ : K), End.maxGenEigenspace (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) i) μ)
      ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (i : L → K), ⨅ (i_1 : L), (↑(genWeightSpaceOf M (i i_1) i_1) : Submodule K M)) ⊤

Tactic:
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_

Premises used: LieModule.genWeightSpaceOf, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, LieSubmodule.lie_mem, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ ∀ (i : L),
    Eq.{u_4 + 1} (α := Submodule K M)
      (⨆ (μ : K), End.maxGenEigenspace (((toEnd K L M : LieHom.{u_1, u_3, u_4} K L (End K M)) : (a : L) → End K M) i) μ)
      ⊤

Tactic:
apply IsTriangularizable.maxGenEigenspace_eq_top

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤

Tactic:
have := iSup_genWeightSpace_eq_top K L M
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
this : Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : L → K), genWeightSpace M χ) ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M)
    (⨆ (x : Weight K L M),
      genWeightSpace M
        (↑((Weight.equivSetOf K L M : (a : Weight K L M) → (↑{χ : L → K | genWeightSpace M χ ≠ ⊥} : Type (max u_1 u_3)))
              x) :
          L → K))
    ⊤

Tactic:
erw [← iSup_ne_bot_subtype, ← (Weight.equivSetOf K L M).iSup_comp] at this

Premises used: Equiv.iSup_comp, LieModule.Weight.equivSetOf, iSup_ne_bot_subtype
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
this :
  Eq.{u_4 + 1} (α := LieSubmodule K L M)
    (⨆ (x : Weight K L M),
      genWeightSpace M
        (↑((Weight.equivSetOf K L M : (a : Weight K L M) → (↑{χ : L → K | genWeightSpace M χ ≠ ⊥} : Type (max u_1 u_3)))
              x) :
          L → K))
    ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : Weight K L M), genWeightSpace M (⇑χ : (a : L) → K)) ⊤

Tactic:
this