awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)

Tactic:
have h_b_eq : (b : L) = x - a := by rw [← h_sum, add_sub_cancel_left]
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
rw : x - (↑a : L) ∈ I
⊢ (↑b : L) ∈ I

Tactic:
rw [h_b_eq]
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
⊢ x - (↑a : L) ∈ I

Tactic:
I.toSubmodule.sub_mem hxI haI

Premises used: Set.Mem, LieSubmodule.toSubmodule, Submodule.sub_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
⊢ x - (↑a : L) ∈ I

Tactic:
exact I.toSubmodule.sub_mem hxI haI

Premises used: LieSubmodule.toSubmodule, Submodule.sub_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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

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
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ 0 ∈ (↑span_compl_roots : Submodule K ↥H)

Tactic:
subst this
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
⊢ a + 0 = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH

Tactic:
subst this
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ (↑0 : L) ∈ I

Tactic:
subst this
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ a = Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH

Tactic:
simp only [add_zero] at hab

Premises used: add_zero
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH ∈ (↑span_I_roots : Submodule K ↥H)

Tactic:
subst hab
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hxH) : L) ∈ I

Tactic:
subst hab