awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
hspan_compl_roots_vanish :
  ∀ (μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ),
    (↑span_compl_roots : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
hx_top : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ (↑span_I_roots : Submodule K ↥H)
b : ↥H
hb : b ∈ (↑span_compl_roots : Submodule K ↥H)
hab : a + b = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
haI : (↑a : L) ∈ I
hbI : (↑b : L) ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have hμ_root : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) μ
Tactic: have hμ_root : μ ∈ H.root := by simpa [LieSubalgebra.root] using 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
hspan_compl_roots_vanish :
  ∀ (μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ),
    (↑span_compl_roots : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
hx_top : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ (↑span_I_roots : Submodule K ↥H)
b : ↥H
hb : b ∈ (↑span_compl_roots : Submodule K ↥H)
hab : a + b = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
haI : (↑a : L) ∈ I
hbI : (↑b : L) ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
hμ_root : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) μ
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have pos : ∀
  (hμI :
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
      (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) μ hμ_root)),
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
Tactic: by_cases hμI : (⟨μ, hμ_root⟩ : H.root) ∈ I.rootSet
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
hspan_compl_roots_vanish :
  ∀ (μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ),
    (↑span_compl_roots : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
hx_top : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ (↑span_I_roots : Submodule K ↥H)
b : ↥H
hb : b ∈ (↑span_compl_roots : Submodule K ↥H)
hab : a + b = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
haI : (↑a : L) ∈ I
hbI : (↑b : L) ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
hμ_root : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) μ
pos :
  ∀
    (hμI :
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) μ hμ_root)),
    Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have neg : ∀
  (hμI :
    Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) μ hμ_root ∉
      I.rootSet),
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
Tactic: by_cases hμI : (⟨μ, hμ_root⟩ : H.root) ∈ I.rootSet
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
hspan_compl_roots_vanish :
  ∀ (μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ),
    (↑span_compl_roots : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
hx_top : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ (↑span_I_roots : Submodule K ↥H)
b : ↥H
hb : b ∈ (↑span_compl_roots : Submodule K ↥H)
hab : a + b = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
haI : (↑a : L) ∈ I
hbI : (↑b : L) ∈ I
μ : Weight K (↥H) L
hμ : ¬μ.IsNonZero
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have hμ₁ : μ.IsZero
Tactic: simp only [Weight.IsNonZero, not_not] at hμ
Cleared hypotheses: 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
have by_contra : ∀ (hα_not : α ∉ I.rootSet), 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
⊢ 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 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
⊢ LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
have rw : Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet ⊆
  (↑(LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
        ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)))) :
    Set (Dual K ↥H))
Tactic: rw [LieIdeal.rootSpan, Submodule.span_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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
γ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hγ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet γ
⊢ Membership.mem (α := Dual.{u_1, u_2} K ↥H)
    (↑(LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
          ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)))) :
      Set (Dual K ↥H))
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) γ : Dual.{u_1, u_2} K ↥H)
have simp : Eq.{u_1 + 1} (α := K)
  ((Weight.toLinear K (↥H) L (↑γ : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑α : Weight K (↥H) L)) : K) (0 : K)
Tactic: simp only [SetLike.mem_coe, LinearMap.mem_ker, Dual.eval_apply, rootSystem_root_apply]
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
⊢ False
have this : LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
  (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
    ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
Tactic: have : I.rootSpan ≤ LinearMap.ker (Dual.eval K H (coroot (α : Weight K H L))) := by
    rw [LieIdeal.rootSpan, Submodule.span_le]
    rintro _ ⟨γ, hγ, rfl⟩
    simp only [SetLike.mem_coe, LinearMap.mem_ker, Dual.eval_apply, rootSystem_root_apply]
    exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hγ hα_not
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
⊢ False
have this₁ : Eq.{u_1 + 1} (α := K)
  ((((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)) : Dual K (Dual.{u_1, u_2} K ↥H)) :
        (a : Dual K ↥H) → K)
      (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) :
    K)
  (0 : K)
Tactic: have := LinearMap.mem_ker.mp (this hα_span)
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα_span :
  Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L))
hα_not : α ∉ I.rootSet
hα_nz : (↑α : Weight K (↥H) L).IsNonZero
this_1 :
  LE.le (α := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan
    (LinearMap.ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K)
      ((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L))))
this :
  Eq.{u_1 + 1} (α := K)
    ((((Dual.eval K ↥H : (a : ↥H) → Dual K (Dual K ↥H)) (coroot (↑α : Weight K (↥H) L)) :
            Dual K (Dual.{u_1, u_2} K ↥H)) :
          (a : Dual K ↥H) → K)
        (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) :
      K)
    (0 : K)
⊢ False
have this₁ : Eq.{u_1 + 1} (α := K) 2 0
Tactic: simp only [Dual.eval_apply, Weight.toLinear_apply, root_apply_coroot hα_nz] at this
Cleared hypotheses: this
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯
have a : LieSubmodule.restr I H ≤
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), sl2SubmoduleOfRoot sorry
Tactic: apply le_antisymm
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
a :
  LieSubmodule.restr I H ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯
⊢ LieSubmodule.restr I H =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯
have a₁ : ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      sl2SubmoduleOfRoot sorry ≤
  LieSubmodule.restr I H
Tactic: apply le_antisymm
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯
have a : LE.le.{u_2} (α := LieSubmodule K (↥H) L)
  ((⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)) ⊔
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      sl2SubmoduleOfRoot sorry)
Tactic: rw [lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, restr_inf_cartan_eq_biSup_corootSubmodule]
-- 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    ((⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L)) ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
have a : LE.le.{u_2} (α := LieSubmodule K (↥H) L)
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      corootSubmodule (↑α : Weight K (↥H) L))
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      sl2SubmoduleOfRoot sorry)
Tactic: apply 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 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
a :
  LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
⊢ LE.le.{u_2} (α := LieSubmodule K (↥H) L)
    ((⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L)) ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        sl2SubmoduleOfRoot ⋯)
have a₁ : LE.le.{u_2} (α := LieSubmodule K (↥H) L)
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
      rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K))
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      sl2SubmoduleOfRoot sorry)
Tactic: apply sup_le