-- 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:
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, ((toEnd k L ↥W) z).HasEigenvalue c

Tactic:
have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))

Result:
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
⊢ ∃ c, ((toEnd k L ↥W) z).HasEigenvalue c

Proof state:
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
⊢ z ≠ 0

Tactic:
aesop

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
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
let e : (k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z <| by aesop).symm

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
⊢ ∃ χ, 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
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅↑(π₂ x), v⁆ = (c • e (π₂ x)) • v

Tactic:
calc ⁅(π₂ x : L), v⁆
    = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W) := by rw [← he, smul_lie, ← hvc.apply_eq_smul]; rfl
  _ = (c • e (π₂ x)) • v              := by rw [smul_assoc, smul_comm]; rfl

Result:
no goals

Proof state:
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
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅↑(π₂ x), v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩)

Tactic:
rw [← he, smul_lie, ← hvc.apply_eq_smul]

Result:
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
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ⁅z, v⁆ = e (π₂ x) • ↑(((toEnd k L ↥W) z) ⟨v, hv⟩)