awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 α
⊢ 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)
have mp : ∀ (hα_not : ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) ∉ q),
  False
Tactic: by_contra hα_not
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ False
have hα_nz : (↑α : Weight K (↥H) L).IsNonZero
Tactic: have hα_nz := H.isNonZero_coe_root α
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ False
have 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)
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χ)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 χ
have 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) β sorry) :
        Weight K (↥H) L))
      sorry ≤
    ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
Tactic: refine iSup_le fun ⟨β, hβ_mem, hβ_nz⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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
⊢ 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 χ
have rw : genWeightSpace L
        (⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β sorry) :
              Weight K (↥H) L) :
          (a : ↥H) → K) ⊔
      genWeightSpace L
        (-(⇑(↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β sorry) :
                Weight K (↥H) L) :
            (a : ↥H) → K)) ⊔
    corootSubmodule
      (↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β sorry) :
        Weight K (↥H) L) ≤
  ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 χ
have 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) β sorry) :
          Weight K (↥H) L) :
      (a : ↥H) → K))
  (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 χ)
⊢ 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 χ
have 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) β sorry) :
            Weight K (↥H) L) :
        (a : ↥H) → K)))
  (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ)
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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 χ)
⊢ 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 χ
have refine_3 : corootSubmodule
    (↑(Subtype.mk (p := fun (α : Weight K (↥H) L) ↦ Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero) β sorry) :
      Weight K (↥H) L) ≤
  ⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)), genWeightSpace L χ
Tactic: refine sup_le (sup_le ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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
have rw : -Weight.toLinear K (↥H) L β ∈ q
Tactic: rw [Weight.toLinear_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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 χ)
have this : Weight.toLinear K (↥H) L (-β) ∈ q
Tactic: have : ↑(-β) ∈ q := by rw [Weight.toLinear_neg]; exact q.neg_mem hβ_mem
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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
⊢ 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 χ
have refine_3 : rootSpace H 0 ≤ ⨆ (χ : ↥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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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)
⊢ False
have h_le : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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 χ
⊢ False
have 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))
Tactic: have h_disj := ((iSupIndep_genWeightSpace K H L _).mono_right h_le).mono_right hα_mem
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
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) ≤ sl2SubmoduleOfRoot ⋯
have 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)
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]