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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
⊢ genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I

Tactic:
have h_plus_contain : genWeightSpace L (χ.toLinear + α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (q.add_mem h_chi_in_q hαq) w_plus
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
⊢ -Weight.toLinear K (↥H) L α = HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α)

Tactic:
have : -α.toLinear = (-1 : K) • α.toLinear := by simp
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
this : -Weight.toLinear K (↥H) L α = HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α)
rw : Weight.toLinear K (↥H) L χ + HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α) ∈ q
⊢ Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ∈ q

Tactic:
rw [sub_eq_add_neg, this]

Premises used: sub_eq_add_neg
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
this : -Weight.toLinear K (↥H) L α = HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α)
⊢ Weight.toLinear K (↥H) L χ + HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α) ∈ q

Tactic:
q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)

Premises used: Set.Mem, OfNat.ofNat, Neg.neg, Submodule.smul_mem, Submodule.add_mem
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
this : -Weight.toLinear K (↥H) L α = HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α)
⊢ Weight.toLinear K (↥H) L χ + HSMul.hSMul (α := K) (-1) (Weight.toLinear K (↥H) L α) ∈ q

Tactic:
exact q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)

Premises used: OfNat.ofNat, Neg.neg, Submodule.smul_mem, Submodule.add_mem
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
⊢ genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I

Tactic:
have h_minus_contain : genWeightSpace L (χ.toLinear - α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (by
      have : -α.toLinear = (-1 : K) • α.toLinear := by simp
      rw [sub_eq_add_neg, this]
      exact q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)) w_minus
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
h_minus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
⊢ genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K) ≤ I

Tactic:
have h_chi_contain : genWeightSpace L χ.toLinear ≤ I :=
    genWeightSpace_le_I _ h_chi_in_q (fun h_eq => (w_chi h_eq).elim)
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
h_minus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
h_chi_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K) ≤ I
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆

Tactic:
sup_le (sup_le h_plus_contain h_minus_contain) h_chi_contain h_bracket_decomp

Premises used: Set.Mem, sup_le
-- 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)
χ : 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
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 : 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_in_q : Weight.toLinear K (↥H) L χ ∈ q
h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
h_bracket_decomp :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ⊔
        genWeightSpace L
          (HSub.hSub (α := (a : ↥H) → K) (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K)
            (⇑(Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊔
      genWeightSpace L (⇑χ : (a : ↥H) → K))
    ⁅x_χ, m_α⁆
I : LieSubmodule K (↥H) L :=
  ⨆ (β : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I :
  ∀ (β_lin : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) (hβ_in_q : β_lin ∈ q) (hβ_ne_zero : β_lin ≠ 0),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
h_plus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
h_minus_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K) ≤ I
h_chi_contain : genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) : (a : ↥H) → K) ≤ I
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆

Tactic:
exact sup_le (sup_le h_plus_contain h_minus_contain) h_chi_contain h_bracket_decomp

Premises used: sup_le
-- 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
γ : Weight K (↥H) L
hγ : γ.IsNonZero
⊢ Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) γ

Tactic:
simpa [LieSubalgebra.root]

Premises used: LieSubalgebra.root