Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

pp: case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
⊢ -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
⊢ -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')