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))
⊢ 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 hx_top : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ span_I_roots ⊔ span_compl_roots
Tactic: have hx_top : (⟨x, hxH⟩ : H) ∈ span_I_roots ⊔ span_compl_roots := h_top ▸ trivial
-- 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
⊢ 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 obtain : ∀ (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),
  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: obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hx_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 α
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
⊢ 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 : (↑a : L) ∈ I
Tactic: have haI : (a : L) ∈ I :=
    (iSup₂_le (fun _ hα ↦ I.corootSubmodule_le hα) :
      ⨆ α ∈ I.rootSet, corootSubmodule α.1 ≤ _)
      (hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha)
-- 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
⊢ (↑b : L) ∈ I
have h_sum : (↑a : L) + (↑b : L) = x
Tactic: have h_sum : (a : L) + b = x := congr_arg Subtype.val 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
h_sum : (↑a : L) + (↑b : L) = x
⊢ (↑b : L) = x - (↑a : L)
have rw : (↑b : L) = (↑a : L) + (↑b : L) - (↑a : L)
Tactic: rw [← h_sum, add_sub_cancel_left]
-- 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
h_sum : (↑a : L) + (↑b : L) = x
rw : (↑b : L) = (↑a : L) + (↑b : L) - (↑a : L)
⊢ (↑b : L) = x - (↑a : L)
have rw₁ : (↑b : L) = (↑b : L)
Tactic: rw [← h_sum, add_sub_cancel_left]
-- 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
h_sum : (↑a : L) + (↑b : L) = x
⊢ (↑b : L) ∈ I
have h_b_eq : (↑b : L) = x - (↑a : L)
Tactic: have h_b_eq : (b : L) = x - a := by rw [← h_sum, add_sub_cancel_left]
-- 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
h_sum : (↑a : L) + (↑b : L) = x
h_b_eq : (↑b : L) = x - (↑a : L)
⊢ (↑b : L) ∈ I
have rw : x - (↑a : L) ∈ I
Tactic: rw [h_b_eq]
-- 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
⊢ 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 : (↑b : L) ∈ I
Tactic: have hbI : (b : L) ∈ I := by
    have h_sum : (a : L) + b = x := congr_arg Subtype.val hab
    have h_b_eq : (b : L) = x - a := by rw [← h_sum, add_sub_cancel_left]
    rw [h_b_eq]; exact I.toSubmodule.sub_mem hxI haI
-- 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
⊢ 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 hb₁ : 0 ∈ (↑span_compl_roots : Submodule K ↥H)
Tactic: subst this
Cleared hypotheses: b, hb, hab, hbI, this