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 : 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α : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : β ∉ I.rootSet
h_ker :
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑β : Weight K (↥H) L)))
    (coroot (↑α : Weight K (↥H) L))
⊢ Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑β : Weight K (↥H) L)) : K) (0 : K)
have change : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑α : Weight K (↥H) L))) (coroot (↑β : Weight K (↥H) L))
Tactic: change coroot (β : Weight K H L) ∈ (α : Weight K H L).ker
-- 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α : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : β ∉ I.rootSet
h_ker :
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑β : Weight K (↥H) L)))
    (coroot (↑α : Weight K (↥H) L))
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑α : Weight K (↥H) L)))
    (coroot (↑β : Weight K (↥H) L))
have rw : Eq.{u_1 + 1} (α := K)
  ((LinearMap.BilinForm.toLinHomAux₁ (traceForm K (↥H) L) (coroot (↑α : Weight K (↥H) L)) : (a : ↥H) → K)
      (coroot (↑β : Weight K (↥H) L)) :
    K)
  (0 : K)
Tactic: rw [← orthogonal_span_coroot_eq_ker,
    LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LinearMap.mem_ker]
-- 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 ⊓ H.toLieSubmodule =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
have refine : LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      corootSubmodule (↑α : Weight K (↥H) L)
Tactic: refine le_antisymm ?_ (iSup₂_le fun _ hα ↦
    le_inf (I.corootSubmodule_le hα) LieSubmodule.map_incl_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
x : L
⊢ x ∈ LieSubmodule.restr I H ⊓ H.toLieSubmodule →
    Membership.mem (γ := 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))
      x
have this : ∀ (hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L))
  (hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)),
  Membership.mem (γ := 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))
    x
Tactic: ⟨hxI, hxH⟩
-- 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 β
⊢ Membership.mem (γ := 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))
    x
have h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
Tactic: have h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α :=
    (iSup_split f (· ∈ I.rootSet)).symm
-- 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 α
⊢ span_I_roots ⊔ span_compl_roots = ⊤
have rw : LE.le.{u_2} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K))
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α)
Tactic: rw [h_split, eq_top_iff, ← biSup_corootSpace_eq_top]
-- 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 α
⊢ Membership.mem (γ := 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))
    x
have h_top : span_I_roots ⊔ span_compl_roots = ⊤
Tactic: have h_top : span_I_roots ⊔ span_compl_roots = ⊤ := by
    rw [h_split, eq_top_iff, ← biSup_corootSpace_eq_top]
    exact iSup₂_le fun α hα ↦ le_iSup_of_le ⟨α, by simpa [LieSubalgebra.root] using hα⟩ le_rfl
-- 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 = ⊤
⊢ 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)
have change : LieSubmodule.map H.toLieSubmodule.incl
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α) =
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      corootSubmodule (↑α : Weight K (↥H) L)
Tactic: change LieSubmodule.map _ (⨆ α ∈ I.rootSet, f α) = ⨆ α ∈ 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 = ⊤
⊢ LieSubmodule.map H.toLieSubmodule.incl
      (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α) =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
have simp_rw : Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
  (⨆ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet i),
      LieSubmodule.map H.toLieSubmodule.incl (f i))
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      corootSubmodule (↑α : Weight K (↥H) L))
Tactic: simp_rw [LieSubmodule.map_iSup]
-- 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 = ⊤
⊢ Membership.mem (γ := 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))
    x
have 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)
Tactic: have hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
      ⨆ α ∈ I.rootSet, corootSubmodule α.1 := by
    change LieSubmodule.map _ (⨆ α ∈ I.rootSet, f α) = ⨆ α ∈ I.rootSet, _
    simp_rw [LieSubmodule.map_iSup]; 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 : 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)
μ : ↥(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))
have this : (↑span_compl_roots : Submodule K ↥H) =
  ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H)
Tactic: have : span_compl_roots.toSubmodule = ⨆ β ∉ I.rootSet, (f β).toSubmodule := by
      simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]
-- 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)
μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ
this :
  (↑span_compl_roots : Submodule K ↥H) =
    ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H)
⊢ (↑span_compl_roots : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
have rw : LE.le.{u_2} (α := Submodule K ↥H)
  (⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H))
  (Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L)))
Tactic: rw [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
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)
μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ
this :
  (↑span_compl_roots : Submodule K ↥H) =
    ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H)
γ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hγ : γ ∉ I.rootSet
⊢ (↑(f γ) : Submodule K ↥H) ≤ Weight.ker (M := L) (χ := (↑μ : Weight K (↥H) L))
have rw : 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: rw [coe_corootSpace_eq_span_singleton, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker]
-- 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)
⊢ Membership.mem (γ := 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))
    x
have 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))
Tactic: have hspan_compl_roots_vanish (μ : H.root) (hμ : μ ∈ I.rootSet) :
      span_compl_roots.toSubmodule ≤ μ.1.ker := by
    have : span_compl_roots.toSubmodule = ⨆ β ∉ I.rootSet, (f β).toSubmodule := by
      simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]
    rw [this]
    exact iSup₂_le fun γ hγ ↦ by
      rw [coe_corootSpace_eq_span_singleton, Submodule.span_singleton_le_iff_mem, LinearMap.mem_ker]
      exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hμ hγ