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 ⋯
β_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
neg :
  ∀ (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

Tactic:
by_cases h_trivial : genWeightSpace L β_lin = ⊥

Premises used: LieModule.genWeightSpace, DFunLike.coe
-- 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 ⋯
β_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
h_trivial : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I

Tactic:
simp [h_trivial]
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
⊢ β.IsNonZero

Tactic:
have hβ_nonzero : β.IsNonZero := Weight.coe_toLinear_ne_zero_iff.mp hβ_ne_zero
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I

Tactic:
le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)

Premises used: le_iSup, le_trans
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
neg :
  LE.le (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K))
    (sl2SubmoduleOfRoot (α :=
      (↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
        Weight K (↥H) L))
      ⋯)
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤ I

Tactic:
refine le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)

Premises used: le_iSup, le_trans
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
neg :
  genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤
    genWeightSpace L
          (⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                Weight K (↥H) L) :
            (a : ↥H) → K) ⊔
        genWeightSpace L
          (-(⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                  Weight K (↥H) L) :
              (a : ↥H) → K)) ⊔
      corootSubmodule
        (↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
          Weight K (↥H) L)
⊢ LE.le (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K))
    (sl2SubmoduleOfRoot (α :=
      (↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
        Weight K (↥H) L))
      ⋯)

Tactic:
rw [sl2SubmoduleOfRoot_eq_sup]

Premises used: LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤
    genWeightSpace L
          (⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                Weight K (↥H) L) :
            (a : ↥H) → K) ⊔
        genWeightSpace L
          (-(⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                  Weight K (↥H) L) :
              (a : ↥H) → K)) ⊔
      corootSubmodule
        (↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
          Weight K (↥H) L)

Tactic:
le_sup_of_le_left (le_sup_of_le_left le_rfl)

Premises used: le_rfl, Set.Mem, le_sup_of_le_left
-- 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 ⋯
β_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
h_trivial : ¬Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β_lin : (a : ↥H) → K)) ⊥
β : Weight K (↥H) L := { toFun := (⇑β_lin : (a : ↥H) → K), genWeightSpace_ne_bot' := h_trivial }
hβ_nonzero : β.IsNonZero
⊢ genWeightSpace L (⇑β_lin : (a : ↥H) → K) ≤
    genWeightSpace L
          (⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                Weight K (↥H) L) :
            (a : ↥H) → K) ⊔
        genWeightSpace L
          (-(⇑(↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
                  Weight K (↥H) L) :
              (a : ↥H) → K)) ⊔
      corootSubmodule
        (↑(Subtype.mk (p := fun (β : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero) β ⋯) :
          Weight K (↥H) L)

Tactic:
exact le_sup_of_le_left (le_sup_of_le_left le_rfl)

Premises used: le_rfl, le_sup_of_le_left
-- 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 ⋯
⊢ ∀ (β_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

Tactic:
have genWeightSpace_le_I (β_lin : H →ₗ[K] K) (hβ_in_q : β_lin ∈ q)
      (hβ_ne_zero : β_lin ≠ 0) : genWeightSpace L β_lin ≤ I := by
    by_cases h_trivial : genWeightSpace L β_lin = ⊥
    · simp [h_trivial]
    · let β : Weight K H L := ⟨β_lin, h_trivial⟩
      have hβ_nonzero : β.IsNonZero := Weight.coe_toLinear_ne_zero_iff.mp hβ_ne_zero
      refine le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)
      rw [sl2SubmoduleOfRoot_eq_sup]
      exact le_sup_of_le_left (le_sup_of_le_left le_rfl)