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
this : b = 0
hb₁ : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
⊢ 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 hab₁ : a + 0 = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
Tactic: subst this
Cleared hypotheses: b, hb, hab, hbI, this
-- 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
this : b = 0
hb₁ : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
hab₁ : a + 0 = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
⊢ 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 hbI₁ : (↑0 : L) ∈ I
Tactic: subst this
Cleared hypotheses: b, hb, hab, hbI, this
-- 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)
haI : (↑a : L) ∈ I
hb : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
hab : a + 0 = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
hbI : (↑0 : L) ∈ I
⊢ 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 hab₁ : a = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
Tactic: simp only [add_zero] at hab
Cleared hypotheses: hab
-- 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)
haI : (↑a : L) ∈ I
hb : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
hbI : (↑0 : L) ∈ I
hab : a = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
⊢ 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 ha₁ : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ (↑span_I_roots : Submodule K ↥H)
Tactic: subst hab
Cleared hypotheses: a, ha, haI, hab
-- 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)
haI : (↑a : L) ∈ I
hb : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
hbI : (↑0 : L) ∈ I
hab : a = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH
ha₁ : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ (↑span_I_roots : Submodule K ↥H)
⊢ 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 haI₁ : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH) : L) ∈ I
Tactic: subst hab
Cleared hypotheses: a, ha, haI, hab
-- 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
⊢ 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 suffices : b = 0
Tactic: suffices b = 0 by
    subst this; simp only [add_zero] at hab; subst hab
    exact hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha
-- 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
⊢ b = 0
have suffices : Membership.mem (γ := Submodule K ↥H) (⨅ (α : Weight K (↥H) L), Weight.ker (M := L) (χ := α)) b
Tactic: suffices b ∈ ⨅ α : Weight K H L, α.ker by simpa [iInf_ker_weight_eq_bot] using 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)
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
⊢ Membership.mem (γ := Submodule K ↥H) (⨅ (α : Weight K (↥H) L), Weight.ker (M := L) (χ := α)) b
have refine : ∀ (μ : Weight K (↥H) L), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
Tactic: refine (Submodule.mem_iInf _).mpr fun μ ↦ ?_
-- 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
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have pos : ∀ (hμ : μ.IsNonZero), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
Tactic: by_cases hμ : μ.IsNonZero
-- 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
pos : ∀ (hμ : μ.IsNonZero), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
have neg : ∀ (hμ : ¬μ.IsNonZero), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := μ)) b
Tactic: by_cases hμ : μ.IsNonZero