awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_ne_bot :
  ¬Eq (α := LieSubmodule K (↥H) L)
      (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
γ : Weight K (↥H) L :=
  {
    toFun :=
      HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
        (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := h_minus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L (-α)
⊢ Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) γ

Tactic:
simpa [LieSubalgebra.root]

Premises used: LieSubalgebra.root
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_ne_bot :
  ¬Eq (α := LieSubmodule K (↥H) L)
      (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
γ : Weight K (↥H) L :=
  {
    toFun :=
      HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
        (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := h_minus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L (-α)
⊢ Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H))
    (Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)

Tactic:
exact ⟨⟨γ, by simpa [LieSubalgebra.root]⟩, rfl⟩
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_ne_bot :
  ¬Eq (α := LieSubmodule K (↥H) L)
      (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
γ : Weight K (↥H) L :=
  {
    toFun :=
      HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
        (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := h_minus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L (-α)
h_sum_in_range :
  Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H))
    (HAdd.hAdd (α := Dual.{u_1, u_2} K ↥H) (β := Dual.{u_1, u_2} K ↥H)
      ((S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)
      ((S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j : Dual.{u_1, u_2} K ↥H))
⊢ ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(S.reflection i) : Dual K ↥H →ₗ[K] Dual K ↥H)

Tactic:
exact hq
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥

Tactic:
have h_minus_bot : genWeightSpace L (χ.toLinear - α.toLinear) = ⊥ := by
    by_contra h_minus_ne_bot
    let γ : Weight K H L := ⟨χ.toLinear - α.toLinear, h_minus_ne_bot⟩
    have hγ_nonzero : γ.IsNonZero := Weight.coe_toLinear_ne_zero_iff.mp w_minus
    obtain ⟨i, hi⟩ := exists_root_index χ (Weight.coe_toLinear_ne_zero_iff.mp w_chi)
    obtain ⟨j, hj⟩ := exists_root_index (-α) (Weight.IsNonZero.neg hα₀)
    have h_sum_in_range : S.root i + S.root j ∈ Set.range S.root := by
      rw [hi, hj, Weight.toLinear_neg, ← sub_eq_add_neg]
      exact ⟨⟨γ, by simpa [LieSubalgebra.root]⟩, rfl⟩
    have h_equiv := RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule
      ⟨q, by rw [RootPairing.mem_invtRootSubmodule_iff]; exact hq⟩ h_sum_in_range
    rw [hi] at h_equiv
    exact h_chi_not_in_q (h_equiv.mpr (by
      rw [hj, Weight.toLinear_neg]
      convert! q.smul_mem (-1) hαq using 1
      rw [neg_smul, one_smul]))
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
obtain :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ),
    Membership.mem (γ := LieSubmodule K (↥H) L)
      (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆

Tactic:
obtain ⟨i, hi⟩ := exists_root_index χ (Weight.coe_toLinear_ne_zero_iff.mp w_chi)

Premises used: Iff.mp, LieModule.Weight.coe_toLinear_ne_zero_iff
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
obtain :
  ∀ (j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α),
    Membership.mem (γ := LieSubmodule K (↥H) L)
      (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆

Tactic:
obtain ⟨j, hj⟩ := exists_root_index α hα₀
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_eq : i = j
⊢ False

Tactic:
exact w_minus (by rw [← hi, ← hj, h_eq, sub_self])
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
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
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_eq :
  Eq (α := Dual.{u_1, u_2} K ↥H) ((S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)
    (-(S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j : Dual.{u_1, u_2} K ↥H)
⊢ False

Tactic:
exact w_plus (by rw [← hi, ← hj, h_eq, neg_add_cancel])