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)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
x₁ x₂ : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₁
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₂
ih₁ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x₁, m⁆
ih₂ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x₂, m⁆
⊢ Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (⁅x₁, m⁆ + ⁅x₂, m⁆)

Tactic:
add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
x₁ x₂ : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₁
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₂
ih₁ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x₁, m⁆
ih₂ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x₂, m⁆
⊢ Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (⁅x₁, m⁆ + ⁅x₂, m⁆)

Tactic:
exact add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ (↑(invtSubmoduleToLieIdeal q hq) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)

Tactic:
rfl

Premises used: Set.Mem, setOf, 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)
rw :
  (↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₁ :
  (↑(invtSubmoduleToLieIdeal q hq) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₂ :
  Eq.{u_2 + 1} (α := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := Submodule K L)
    (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
      (↑(sl2SubmoduleOfRoot ⋯) : Submodule K L))
    (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
      (↑(sl2SubmoduleOfRoot ⋯) : Submodule K L))
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H =
    ⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.toSubmodule_inj, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.restr_toSubmodule
-- 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))
set :
  let J := invtSubmoduleToLieIdeal q hq;
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    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)
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (invtSubmoduleToLieIdeal q hq).rootSet α ↔
    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)

Tactic:
set J := invtSubmoduleToLieIdeal q hq

Premises used: LieAlgebra.IsKilling.invtSubmoduleToLieIdeal
-- 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
mp :
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α →
    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)
mpr :
  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) →
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    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)

Tactic:
constructor
-- 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 α
mp :
  ∀ (hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q),
    False
⊢ 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)

Tactic:
by_contra hα_not
-- 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
⊢ (↑α : Weight K (↥H) L).IsNonZero

Tactic:
have hα_nz := H.isNonZero_coe_root α
-- 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
χ : Weight K (↥H) L
hχ : Weight.toLinear K (↥H) L χ ∈ q
heq : Eq (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ 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)

Tactic:
simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ

Premises used: LieAlgebra.IsKilling.rootSystem_root_apply
-- 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
⊢ ∀ (χ : 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)

Tactic:
have hne (χ : Weight K H L) (hχ : ↑χ ∈ q) : (χ : H → K) ≠ ((α : Weight K H L) : H → K) :=
      fun heq ↦ hα_not (by simpa [rootSystem_root_apply] using DFunLike.coe_injective heq ▸ hχ)
-- 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:
iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_

Premises used: iInf, Set.Mem, iSup, Set.iInter, setOf, _private.0.LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal.match_1, LE.le, iSup_le, LieModule.genWeightSpace, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal._proof_4, LieAlgebra.IsKilling.sl2SubmoduleOfRoot
-- 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)
refine :
  ∀ (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),
    sl2SubmoduleOfRoot (α :=
        (↑(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 χ
⊢ LieSubmodule.restr J H ≤ ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

Tactic:
refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_

Premises used: iSup_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 :
  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) ≤
    ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
⊢ sl2SubmoduleOfRoot (α :=
      (↑(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:
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)
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
⊢ 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) ≤
    ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

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 : 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_1 :
  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 χ)
refine_2 :
  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 χ)
refine_3 :
  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 χ
⊢ 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) ≤
    ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ

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

Premises used: sup_le