awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet β
⊢ corootSubmodule (↑β : Weight K (↥H) L) ≤ sl2SubmoduleOfRoot ⋯
have rw : corootSubmodule (↑β : Weight K (↥H) L) ≤
  genWeightSpace L (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ⊔
      genWeightSpace L (-(⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
    corootSubmodule (↑β : Weight K (↥H) L)
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ sl2SubmoduleOfRoot ⋯
have rw : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
  genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
      genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
    corootSubmodule (↑α : Weight K (↥H) L)
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ sl2SubmoduleOfRoot ⋯ ≤ LieSubmodule.restr I H
have rw : genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
      genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
    corootSubmodule (↑α : Weight K (↥H) L) ≤
  LieSubmodule.restr I H
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑α : Weight K (↥H) L) ≤
    LieSubmodule.restr I H
have refine_1 : genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
refine_1 : genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑α : Weight K (↥H) L) ≤
    LieSubmodule.restr I H
have refine_2 : genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ≤ LieSubmodule.restr I H
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
refine_1 : genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
refine_2 : genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ≤ LieSubmodule.restr I H
⊢ genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑α : Weight K (↥H) L) ≤
    LieSubmodule.restr I H
have refine_3 : corootSubmodule (↑α : Weight K (↥H) L) ≤ LieSubmodule.restr I H
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ≤ LieSubmodule.restr I H
have refine_2 : Ne.{u_1 + 1} (α := K) ((-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) (coroot (↑α : Weight K (↥H) L)) : K) (0 : K)
Tactic: apply I.rootSpace_le_of_apply_coroot_ne_zero hα
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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
⊢ Membership.mem (α := L) (γ := LieSubmodule K (↥H) L) (genWeightSpace L 0)
    ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) y : L)
have a : Membership.mem (α := L) H.toLieSubmodule ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) y : L)
Tactic: apply toLieSubmodule_le_rootSpace_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
have h_zero_weight : Membership.mem (α := L) (γ := LieSubmodule K (↥H) L) (genWeightSpace L 0)
  ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) y : L)
Tactic: have h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L (0 : H → K) := by
      apply toLieSubmodule_le_rootSpace_zero
      exact y.property
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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_zero_weight :
  Membership.mem (α := L) (γ := LieSubmodule K (↥H) L) (genWeightSpace L 0)
    ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) y : L)
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
have h : (⇑χ : (a : ↥H) → K) = HAdd.hAdd (α := ↥H → K) (⇑χ : (a : ↥H) → K) 0
Tactic: convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx_χ h_zero_weight
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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_zero_weight :
  Membership.mem (α := L) (γ := LieSubmodule K (↥H) L) (genWeightSpace L 0)
    ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) y : L)
⊢ (⇑χ : (a : ↥H) → K) = HAdd.hAdd (α := ↥H → K) (⇑χ : (a : ↥H) → K) 0
have h : ∀ (h : ↥H), (χ : (a : ↥H) → K) h = HAdd.hAdd (α := ↥H → K) (β := ↥H → K) (⇑χ : (a : ↥H) → K) 0 h
Tactic: ext h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆
have h_h_containment : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) ⁅x_χ, (↑y : L)⁆
Tactic: have h_h_containment : ⁅x_χ, (y : L)⁆ ∈ genWeightSpace L χ := by
    have h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L (0 : H → K) := by
      apply toLieSubmodule_le_rootSpace_zero
      exact y.property
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx_χ h_zero_weight
    ext h; simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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)⁆
⊢ 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_α⁆
have rw : 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_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆)
Tactic: rw [h_bracket_sum]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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)⁆
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆
have 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_α⁆
Tactic: have h_bracket_decomp : ⁅x_χ, m_α⁆ ∈
      genWeightSpace L (χ.toLinear + α.toLinear) ⊔
      genWeightSpace L (χ.toLinear - α.toLinear) ⊔ genWeightSpace L χ := by
    rw [h_bracket_sum]
    exact add_mem (add_mem
      (Submodule.mem_sup_left (Submodule.mem_sup_left h_pos_containment))
      (Submodule.mem_sup_left (Submodule.mem_sup_right h_neg_containment)))
      (Submodule.mem_sup_right h_h_containment)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 ⋯
β_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
have pos : ∀ (h_trivial : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥),
  genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
Tactic: by_cases h_trivial : genWeightSpace L β_lin = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 ⋯
β_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
pos :
  ∀ (h_trivial : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥),
    genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
have neg : ∀ (h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥),
  genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I
Tactic: by_cases h_trivial : genWeightSpace L β_lin = ⊥