awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ LE.le (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β ⋯) :
            Weight K (↥H) L) :
        (a : ↥H) → K))
    (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)

Tactic:
le_iSup₂_of_le _ (hne β hβ_mem) le_rfl

Premises used: le_rfl, Set.Mem, setOf, le_iSup₂_of_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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ LE.le (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β ⋯) :
            Weight K (↥H) L) :
        (a : ↥H) → K))
    (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)

Tactic:
exact le_iSup₂_of_le _ (hne β hβ_mem) le_rfl

Premises used: le_rfl, le_iSup₂_of_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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
rw : -Weight.toLinear K (↥H) L β ∈ q
⊢ Weight.toLinear K (↥H) L (-β) ∈ q

Tactic:
rw [Weight.toLinear_neg]

Premises used: LieModule.Weight.toLinear_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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ -Weight.toLinear K (↥H) L β ∈ q

Tactic:
q.neg_mem hβ_mem

Premises used: Set.Mem, Submodule.neg_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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ -Weight.toLinear K (↥H) L β ∈ q

Tactic:
exact q.neg_mem hβ_mem

Premises used: Submodule.neg_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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ Weight.toLinear K (↥H) L (-β) ∈ q

Tactic:
have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
this : Weight.toLinear K (↥H) L (-β) ∈ q
⊢ LE.le (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-(⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β ⋯) :
              Weight K (↥H) L) :
          (a : ↥H) → K)))
    (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)

Tactic:
le_iSup₂_of_le _ (hne (-β) this) le_rfl

Premises used: le_rfl, Set.Mem, setOf, le_iSup₂_of_le, Neg.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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
this : Weight.toLinear K (↥H) L (-β) ∈ q
⊢ LE.le (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-(⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β ⋯) :
              Weight K (↥H) L) :
          (a : ↥H) → K)))
    (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)

Tactic:
exact le_iSup₂_of_le _ (hne (-β) this) le_rfl

Premises used: le_rfl, le_iSup₂_of_le, Neg.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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
refine_3 : rootSpace H 0 ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
⊢ corootSubmodule
      (↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β ⋯) :
        Weight K (↥H) L) ≤
    ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

Tactic:
apply (LieSubmodule.map_incl_le.trans (rootSpace_zero_eq K L H).symm.le).trans

Premises used: Eq.le, LieAlgebra.rootSpace_zero_eq, LieSubmodule.map_incl_le, LE.le.trans, Eq.symm
-- 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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ rootSpace H 0 ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

Tactic:
le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl

Premises used: le_rfl, Set.Mem, setOf, le_iSup₂_of_le, OfNat.ofNat, Eq.symm
-- 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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
x : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ rootSpace H 0 ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

Tactic:
exact le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl

Premises used: le_rfl, le_iSup₂_of_le, OfNat.ofNat
-- 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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr J H ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

Tactic:
have h_le : J.restr H ≤ ⨆ (χ : H → K) (_ : χ ≠ (α : Weight K H L)), genWeightSpace L χ := by
      refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_
      rw [sl2SubmoduleOfRoot_eq_sup]
      refine sup_le (sup_le ?_ ?_) ?_
      · exact le_iSup₂_of_le _ (hne β hβ_mem) le_rfl
      · have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
        exact le_iSup₂_of_le _ (hne (-β) this) le_rfl
      · apply (LieSubmodule.map_incl_le.trans (rootSpace_zero_eq K L H).symm.le).trans
        exact le_iSup₂_of_le 0 (fun h ↦ hα_nz h.symm) le_rfl
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
h_le : LieSubmodule.restr J H ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
⊢ Disjoint ((fun (χ : ↥H → K) ↦ (genWeightSpace L χ : LieSubmodule K (↥H) L)) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))

Tactic:
have h_disj := ((iSupIndep_genWeightSpace K H L _).mono_right h_le).mono_right hα_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)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
h_le : LieSubmodule.restr J H ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
h_disj :
  Disjoint ((fun (χ : ↥H → K) ↦ (genWeightSpace L χ : LieSubmodule K (↥H) L)) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
⊢ False

Tactic:
(α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)

Premises used: Iff.mp, LieModule.Weight.genWeightSpace_ne_bot, disjoint_self, Subtype.val
-- 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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
hne :
  ∀ (χ : Weight K (↥H) L) (hχ : Weight.toLinear K (↥H) L χ ∈ q),
    Ne (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
h_le : LieSubmodule.restr J H ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
h_disj :
  Disjoint ((fun (χ : ↥H → K) ↦ (genWeightSpace L χ : LieSubmodule K (↥H) L)) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
⊢ False

Tactic:
exact (α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)

Premises used: Iff.mp, LieModule.Weight.genWeightSpace_ne_bot, disjoint_self, Subtype.val
-- 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)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα :
  Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥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