-- Mathlib/Algebra/Lie/LieTheorem.lean
theorem exists_nontrivial_weightSpace_of_lieIdeal [LieModule.IsTriangularizable k L V]
    (A : LieIdeal k L) (hA : IsCoatom A.toSubmodule)
    (χ₀ : Module.Dual k A) [Nontrivial (weightSpace V χ₀)] :
    ∃ (χ : Module.Dual k L), Nontrivial (weightSpace V χ)

Proof state:
case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ v ∈ weightSpace V ⇑(χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂)

Tactic:
rw [mem_weightSpace]

Result:
case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ∀ (x : L), ⁅x, v⁆ = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v

Proof state:
case hf
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
this : Nontrivial ↥W
⊢ ⨆ μ, (((toEnd k L ↥W) z).genEigenspace μ) ?k = ⊤

case k
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
this : Nontrivial ↥W
⊢ ℕ∞

Tactic:
exact LieModule.IsTriangularizable.maxGenEigenspace_eq_top z

Result:
no goals

Proof state:
case intro.intro
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
set W : LieSubmodule k L V := weightSpaceOfIsLieTower k V χ₀

Result:
case intro.intro
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Proof state:
case h.refine_2
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(span k {z}) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(span k {z})), e x • z = ↑x
hA : IsCompl (↑A) (span k {z})
π₁ : L →ₗ[k] ↥A := (↑A).linearProjOfIsCompl (span k {z}) hA
π₂ : L →ₗ[k] ↥(span k {z}) := (span k {z}).linearProjOfIsCompl (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ⟨v, ⋯⟩ ≠ 0

Tactic:
simpa [ne_eq, LieSubmodule.mk_eq_zero] using hvc.right

Result:
no goals