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 : 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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
γ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hγ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet γ
⊢ Eq.{u_1 + 1} (α := K)
    ((Weight.toLinear K (↥H) L (↑γ : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑α : Weight K (↥H) L)) : K) (0 : K)

Tactic:
exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not

Premises used: LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
⊢ LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))

Tactic:
have : I.rootSpan ≤ LinearMap.ker (Dual.eval K H (coroot (α : Weight K H L))) := by
    rw [LieIdeal.rootSpan, Submodule.span_le]
    rintro _ ⟨γ, hγ, rfl⟩
    simp only [SetLike.mem_coe, LinearMap.mem_ker, Dual.eval_apply, rootSystem_root_apply]
    exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
⊢ Eq.{u_1 + 1} (α := K)
    ((((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)) :
            Dual K (Dual.{u_1, u_2} K ↥H)) :
          (a : Dual K ↥H) → K)
        (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) :
      K)
    (0 : K)

Tactic:
have := LinearMap.mem_ker.mp (this hα_span)
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this_1 :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
this :
  Eq.{u_1 + 1} (α := K)
    ((((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)) :
            Dual K (Dual.{u_1, u_2} K ↥H)) :
          (a : Dual K ↥H) → K)
        (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) :
      K)
    (0 : K)
⊢ Eq.{u_1 + 1} (α := K) 2 0

Tactic:
simp only [Dual.eval_apply, Weight.toLinear_apply, root_apply_coroot hα_nz] at this

Premises used: Module.Dual.eval_apply, LieAlgebra.IsKilling.root_apply_coroot, LieModule.Weight.toLinear_apply
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this_1 :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
this : Eq.{u_1 + 1} (α := K) 2 0
⊢ False

Tactic:
absurd this two_ne_zero

Premises used: two_ne_zero, absurd
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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α_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this_1 :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
this : Eq.{u_1 + 1} (α := K) 2 0
⊢ False

Tactic:
exact absurd this two_ne_zero

Premises used: two_ne_zero, absurd
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
a :
  LieSubmodule.restr I H ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯
a₁ :
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯ ≤
    LieSubmodule.restr I H
⊢ LieSubmodule.restr I H =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
a :
  LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    ((⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L)) ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
⊢ LieSubmodule.restr I H ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯

Tactic:
rw [lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, restr_inf_cartan_eq_biSup_corootSubmodule]

Premises used: LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
a :
  LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
a₁ :
  LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
⊢ LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    ((⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L)) ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)

Tactic:
apply sup_le

Premises used: sup_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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 β
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)
⊢ corootSubmodule (↑β : Weight K (↥H) L) ≤ sl2SubmoduleOfRoot ⋯

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 : 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) ≤
    genWeightSpace L (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑β : Weight K (↥H) L)

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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) ≤
    genWeightSpace L (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑β : Weight K (↥H) L)

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)

Tactic:
exact iSup₂_le fun β hβ ↦ le_iSup₂_of_le β hβ
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_right)

Premises used: iSup₂_le, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
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)
⊢ rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ sl2SubmoduleOfRoot ⋯

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 : 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) ≤
    genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
le_sup_of_le_left le_sup_left

Premises used: le_sup_left, 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 : 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) ≤
    genWeightSpace L (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ⊔
        genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ⊔
      corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
exact le_sup_of_le_left le_sup_left

Premises used: le_sup_left, 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 : 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
⊢ LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)

Tactic:
exact iSup₂_le fun α hα ↦ le_iSup₂_of_le α hα
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left)

Premises used: iSup₂_le, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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 α
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
⊢ sl2SubmoduleOfRoot ⋯ ≤ LieSubmodule.restr I H

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 : 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

Tactic:
sup_le (sup_le ?_ ?_) ?_

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 : 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
refine_3 : corootSubmodule (↑α : Weight K (↥H) L) ≤ 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

Tactic:
refine sup_le (sup_le ?_ ?_) ?_

Premises used: sup_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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

Tactic:
hα

Premises used: Set.Mem, setOf, LieIdeal.rootSet
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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

Tactic:
exact hα
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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_2 :
  Ne.{u_1 + 1} (α := K) ((-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) (coroot (↑α : Weight K (↥H) L)) : K) (0 : K)
⊢ genWeightSpace L (-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) ≤ LieSubmodule.restr I H

Tactic:
apply I.rootSpace_le_of_apply_coroot_ne_zero hα

Premises used: LieIdeal.rootSpace_le_of_apply_coroot_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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 α
⊢ Ne.{u_1 + 1} (α := K) ((-(⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)) (coroot (↑α : Weight K (↥H) L)) : K) (0 : K)

Tactic:
simp [Pi.neg_apply, root_apply_coroot (H.isNonZero_coe_root α)]

Premises used: LieSubalgebra.isNonZero_coe_root, LieAlgebra.IsKilling.root_apply_coroot, Pi.neg_apply
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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) ≤ LieSubmodule.restr I H

Tactic:
I.corootSubmodule_le hα

Premises used: LieIdeal.corootSubmodule_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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) ≤ LieSubmodule.restr I H

Tactic:
exact I.corootSubmodule_le hα

Premises used: LieIdeal.corootSubmodule_le