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α :
  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)
⊢ 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 : 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)
⊢ 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 : 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)
⊢ sl2SubmoduleOfRoot ⋯ ≤
    ⨆ (x : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯

Tactic:
le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl

Premises used: le_rfl, Set.Mem, LieSubalgebra.isNonZero_coe_root, Subtype.mk, le_iSup_of_le, And.intro, 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)
⊢ ⨆ (x : { β : Weight K (↥H) L // Weight.toLinear K (↥H) L β ∈ q ∧ β.IsNonZero }), sl2SubmoduleOfRoot ⋯ =
    LieSubmodule.restr J H

Tactic:
(restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm

Premises used: LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, 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α :
  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)
calc : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ sl2SubmoduleOfRoot ⋯
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α

Tactic:
calc rootSpace H (α : Weight K H L)
        ≤ sl2SubmoduleOfRoot (H.isNonZero_coe_root α) := by
          rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left
      _ ≤ ⨆ x : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot x.2.2 :=
          le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl
      _ = J.restr H := (restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm

Premises used: LieSubmodule.restr, le_rfl, LieSubalgebra.isNonZero_coe_root, Membership.mem, Subtype, le_iSup_of_le, LieAlgebra.rootSpace, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.sl2SubmoduleOfRoot, Eq.symm, Subtype.val, DFunLike.coe, LieModule.Weight
-- 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₁ 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)
hq₂ :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q₂ ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
h : q₁ ≤ q₂
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q₁ hq₁) H ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal q₂ hq₂) H

Tactic:
iSup_le fun ⟨α, hα_mem, hα_nz⟩ ↦ le_iSup_of_le ⟨α, h hα_mem, hα_nz⟩ le_rfl

Premises used: LieSubmodule.restr, iInf, le_rfl, Set.Mem, Set.iInter, setOf, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal, _private.0.LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal.match_1, LE.le, Subtype.mk, le_iSup_of_le, And.intro, iSup_le, 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₁ 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)
hq₂ :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q₂ ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
h : q₁ ≤ q₂
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q₁ hq₁) H ≤ LieSubmodule.restr (invtSubmoduleToLieIdeal q₂ hq₂) H

Tactic:
exact iSup_le fun ⟨α, hα_mem, hα_nz⟩ ↦ le_iSup_of_le ⟨α, h hα_mem, hα_nz⟩ le_rfl

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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
set :
  let J := invtSubmoduleToLieIdeal I.rootSpan ⋯;
  J = I
⊢ invtSubmoduleToLieIdeal I.rootSpan hI = I

Tactic:
set J := invtSubmoduleToLieIdeal I.rootSpan
    ((rootSystem H).mem_invtRootSubmodule_iff.mp I.rootSpan_mem_invtRootSubmodule)

Premises used: LieAlgebra.IsKilling.rootSystem, RootPairing.mem_invtRootSubmodule_iff, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal, LieIdeal.rootSpan, Iff.mp
-- 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
rw :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
      (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]

Premises used: LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
      (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, rfl⟩⟩

Premises used: LieIdeal.mem_rootSet_of_mem_rootSpan, And.intro, Iff.intro, Exists.intro, Submodule.subset_span, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
      (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
⊢ ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
have h_eq : ∀ α : H.root, α ∈ J.rootSet ↔ α ∈ I.rootSet := fun α ↦ by
    rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
    exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
rw :
  Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α),
        sl2SubmoduleOfRoot ⋯)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
⊢ LieSubmodule.restr J H = LieSubmodule.restr I H

Tactic:
rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]

Premises used: LieIdeal.restr_eq_iSup_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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α),
        sl2SubmoduleOfRoot ⋯)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)

Tactic:
le_antisymm
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).1 hα) le_rfl)
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).2 hα) le_rfl)

Premises used: Iff.mpr, iSup₂_le, le_rfl, le_antisymm, Iff.mp, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α),
        sl2SubmoduleOfRoot ⋯)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)

Tactic:
exact le_antisymm
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).1 hα) le_rfl)
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).2 hα) le_rfl)

Premises used: Iff.mpr, iSup₂_le, le_rfl, le_antisymm, Iff.mp, 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ LieSubmodule.restr J H = LieSubmodule.restr I H

Tactic:
have h_restr : J.restr H = I.restr H := by
    rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]
    exact le_antisymm
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).1 hα) le_rfl)
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).2 hα) 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
rw : (↑J : Submodule K L) = (↑I : Submodule K L)
rw₁ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑I : Submodule K L)
rw₂ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑(LieSubmodule.restr I H) : Submodule K L)
rw₃ rw₄ : (↑(LieSubmodule.restr I H) : Submodule K L) = (↑(LieSubmodule.restr I H) : Submodule K L)
⊢ J = I

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
    ← LieSubmodule.restr_toSubmodule I H, h_restr]

Premises used: LieSubmodule.toSubmodule_inj, 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 : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
simp :
  Submodule.span K
      (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
            LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}) =
    (↑q : Submodule K (Dual K ↥H))
⊢ (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq).toInvtRootSubmodule = q

Tactic:
simp only [Subtype.ext_iff, LieIdeal.toInvtRootSubmodule, LieIdeal.rootSpan, LieIdeal.rootSet]

Premises used: Subtype.ext_iff, LieIdeal.rootSet, LieIdeal.rootSpan, LieIdeal.toInvtRootSubmodule
-- 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 : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
rw :
  Submodule.span K
    (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
      {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
          ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)})
| (↑q : Submodule K (Dual K ↥H))

Tactic:
rw [RootPairing.invtRootSubmodule.eq_span_root q]

Premises used: RootPairing.invtRootSubmodule.eq_span_root