Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
⊢ b ∈ Weight.ker

pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : ¬μ.IsNonZero
⊢ b ∈ Weight.ker

Tactic:
· have hμ_root : μ ∈ H.root := by simpa [LieSubalgebra.root] using hμ
    by_cases hμI : (⟨μ, hμ_root⟩ : H.root) ∈ I.rootSet
    · exact hspan_compl_roots_vanish ⟨μ, hμ_root⟩ hμI hb
    · exact I.root_apply_eq_zero_of_notMem_rootSet hbI hμI

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : ¬μ.IsNonZero
⊢ b ∈ Weight.ker