Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
β_lin : ↥H →ₗ[K] K
hβ_in_q : β_lin ∈ q
hβ_ne_zero : β_lin ≠ 0
⊢ genWeightSpace L ⇑β_lin ≤ I

Tactic:
by_cases h_trivial : genWeightSpace L β_lin = ⊥

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
β_lin : ↥H →ₗ[K] K
hβ_in_q : β_lin ∈ q
hβ_ne_zero : β_lin ≠ 0
h_trivial : genWeightSpace L ⇑β_lin = ⊥
⊢ genWeightSpace L ⇑β_lin ≤ I

case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
β_lin : ↥H →ₗ[K] K
hβ_in_q : β_lin ∈ q
hβ_ne_zero : β_lin ≠ 0
h_trivial : ¬genWeightSpace L ⇑β_lin = ⊥
⊢ genWeightSpace L ⇑β_lin ≤ I