Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: 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)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
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
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)
y : ↥H.toLieSubmodule
hy : y ∈ ↑↑(corootSpace ⇑α)
hm_eq : m_αneg + ↑H.toLieSubmodule.incl y = m_α
hm_α_decomp : m_α = m_pos + m_neg + ↑H.toLieSubmodule.incl y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑H.toLieSubmodule.incl y⁆
h_chi_in_q : Weight.toLinear K (↥H) L χ ∈ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

pp: 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)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
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
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)
y : ↥H.toLieSubmodule
hy : y ∈ ↑↑(corootSpace ⇑α)
hm_eq : m_αneg + ↑H.toLieSubmodule.incl y = m_α
hm_α_decomp : m_α = m_pos + m_neg + ↑H.toLieSubmodule.incl y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑H.toLieSubmodule.incl y⁆
h_chi_in_q : Weight.toLinear K (↥H) L χ ∉ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
· exact chi_in_q_aux q χ x_χ m_α hx_χ α hαq w_plus w_minus w_chi m_pos m_neg y h_bracket_sum
      h_pos_containment h_neg_containment h_chi_in_q

Goal state after:
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)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
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
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)
y : ↥H.toLieSubmodule
hy : y ∈ ↑↑(corootSpace ⇑α)
hm_eq : m_αneg + ↑H.toLieSubmodule.incl y = m_α
hm_α_decomp : m_α = m_pos + m_neg + ↑H.toLieSubmodule.incl y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑H.toLieSubmodule.incl y⁆
h_chi_in_q : Weight.toLinear K (↥H) L χ ∉ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯