awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) y
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z

Tactic:
simp [iSup_genWeightSpace_eq_top]

Premises used: LieModule.iSup_genWeightSpace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) y
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z

Tactic:
have hz : z ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_genWeightSpace_eq_top]
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z_1 : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
β : ↥H → K
z : L
hz : z ∈ rootSpace H β
⊢ (S : (a : L) → L) ⁅y, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)

Tactic:
h_der y z α β hy hz
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z_1 : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
β : ↥H → K
z : L
hz : z ∈ rootSpace H β
⊢ (S : (a : L) → L) ⁅y, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)

Tactic:
exact h_der y z α β hy hz
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
⊢ (S : (a : L) → L) ⁅y, 0⁆ =
    HAdd.hAdd (α := L) (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) 0 : L)
      (⁅y, (S : (a : L) → L) 0⁆ : L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
x_1 y_2 : L
hx_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1
hy_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_2
h :
  (S : (a : L) → L) ⁅y, x_1⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1) (⁅y, (S : (a : L) → L) x_1⁆ : L)
h' :
  (S : (a : L) → L) ⁅y, y_2⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2) (⁅y, (S : (a : L) → L) y_2⁆ : L)
mem :
  HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1) (⁅y, (S : (a : L) → L) x_1⁆ : L) +
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2) (⁅y, (S : (a : L) → L) y_2⁆ : L) =
    Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1 + Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2 +
      HAdd.hAdd (α := L) (β := L) (⁅y, (S : (a : L) → L) x_1⁆ : L) (⁅y, (S : (a : L) → L) y_2⁆ : L)
⊢ (S : (a : L) → L) ⁅y, x_1 + y_2⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) (x_1 + y_2))
      (⁅y, (S : (a : L) → L) (x_1 + y_2)⁆ : L)

Tactic:
simp only [lie_add, map_add, h, h']

Premises used: map_add, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
x_1 y_2 : L
hx_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1
hy_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_2
h :
  (S : (a : L) → L) ⁅y, x_1⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1) (⁅y, (S : (a : L) → L) x_1⁆ : L)
h' :
  (S : (a : L) → L) ⁅y, y_2⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2) (⁅y, (S : (a : L) → L) y_2⁆ : L)
⊢ HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1) (⁅y, (S : (a : L) → L) x_1⁆ : L) +
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2) (⁅y, (S : (a : L) → L) y_2⁆ : L) =
    Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x_1 + Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2 +
      HAdd.hAdd (α := L) (β := L) (⁅y, (S : (a : L) → L) x_1⁆ : L) (⁅y, (S : (a : L) → L) y_2⁆ : L)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y_1 z : L
hz : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
mem :
  ∀ (β : ↥H → K) (z : L) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
mem₁ :
  (S : (a : L) → L) ⁅y, 0⁆ =
    HAdd.hAdd (α := L) (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) 0 : L)
      (⁅y, (S : (a : L) → L) 0⁆ : L)
mem₂ :
  ∀ (x y_2 : L),
    Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x →
      Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_2 →
        ∀
          (h :
            (S : (a : L) → L) ⁅y, x⁆ =
              HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) x) (⁅y, (S : (a : L) → L) x⁆ : L))
          (h' :
            (S : (a : L) → L) ⁅y, y_2⁆ =
              HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) y_2)
                (⁅y, (S : (a : L) → L) y_2⁆ : L)),
          (S : (a : L) → L) ⁅y, x + y_2⁆ =
            HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) (x + y_2))
              (⁅y, (S : (a : L) → L) (x + y_2)⁆ : L)
⊢ (S : (a : L) → L) ⁅y, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)

Tactic:
induction hz using LieSubmodule.iSup_induction' with
      | mem β z hz => exact h_der y z α β hy hz
      | zero => simp
      | add _ _ _ _ h h' => simp only [lie_add, map_add, h, h']; abel

Premises used: map_add, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hz : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z
⊢ (S : (a : L) → L) (Bracket.bracket (L := L) 0 z) =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) 0 : L) z)
      (Bracket.bracket (L := L) 0 ((S : (a : L) → L) z) : L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hz : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z
x_1 y_1 : L
hx_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_1
h :
  (S : (a : L) → L) ⁅x_1, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z) (⁅x_1, (S : (a : L) → L) z⁆ : L)
h' :
  (S : (a : L) → L) ⁅y_1, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z) (⁅y_1, (S : (a : L) → L) z⁆ : L)
add :
  HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z) (⁅x_1, (S : (a : L) → L) z⁆ : L) +
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z) (⁅y_1, (S : (a : L) → L) z⁆ : L) =
    Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z + Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z +
      HAdd.hAdd (α := L) (β := L) (⁅x_1, (S : (a : L) → L) z⁆ : L) (⁅y_1, (S : (a : L) → L) z⁆ : L)
⊢ (S : (a : L) → L) ⁅x_1 + y_1, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) (x_1 + y_1) : L) z)
      (⁅x_1 + y_1, (S : (a : L) → L) z⁆ : L)

Tactic:
simp only [add_lie, map_add, h, h']

Premises used: map_add, add_lie
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hz : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z
x_1 y_1 : L
hx_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_1
h :
  (S : (a : L) → L) ⁅x_1, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z) (⁅x_1, (S : (a : L) → L) z⁆ : L)
h' :
  (S : (a : L) → L) ⁅y_1, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z) (⁅y_1, (S : (a : L) → L) z⁆ : L)
⊢ HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z) (⁅x_1, (S : (a : L) → L) z⁆ : L) +
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z) (⁅y_1, (S : (a : L) → L) z⁆ : L) =
    Bracket.bracket (L := L) ((S : (a : L) → L) x_1 : L) z + Bracket.bracket (L := L) ((S : (a : L) → L) y_1 : L) z +
      HAdd.hAdd (α := L) (β := L) (⁅x_1, (S : (a : L) → L) z⁆ : L) (⁅y_1, (S : (a : L) → L) z⁆ : L)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
y z : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) y
hz : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) z
mem :
  ∀ (α : ↥H → K) (y : L) (hy : y ∈ rootSpace H α),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
zero :
  (S : (a : L) → L) (Bracket.bracket (L := L) 0 z) =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) 0 : L) z)
      (Bracket.bracket (L := L) 0 ((S : (a : L) → L) z) : L)
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x →
      Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y →
        ∀
          (h :
            (S : (a : L) → L) ⁅x, z⁆ =
              HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) x : L) z) (⁅x, (S : (a : L) → L) z⁆ : L))
          (h' :
            (S : (a : L) → L) ⁅y, z⁆ =
              HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)),
          (S : (a : L) → L) ⁅x + y, z⁆ =
            HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) (x + y) : L) z)
              (⁅x + y, (S : (a : L) → L) z⁆ : L)
⊢ (S : (a : L) → L) ⁅y, z⁆ =
    HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)

Tactic:
induction hy using LieSubmodule.iSup_induction' with
    | mem α y hy =>
      induction hz using LieSubmodule.iSup_induction' with
      | mem β z hz => exact h_der y z α β hy hz
      | zero => simp
      | add _ _ _ _ h h' => simp only [lie_add, map_add, h, h']; abel
    | zero => simp
    | add _ _ _ _ h h' => simp only [add_lie, map_add, h, h']; abel

Premises used: map_add, lie_add, add_lie
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L) (α β : ↥H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
⊢ ∀ (y z : L),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)

Tactic:
replace h_der (y z : L) : S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆ := by
    have hy : y ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_genWeightSpace_eq_top]
    have hz : z ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_genWeightSpace_eq_top]
    induction hy using LieSubmodule.iSup_induction' with
    | mem α y hy =>
      induction hz using LieSubmodule.iSup_induction' with
      | mem β z hz => exact h_der y z α β hy hz
      | zero => simp
      | add _ _ _ _ h h' => simp only [lie_add, map_add, h, h']; abel
    | zero => simp
    | add _ _ _ _ h h' => simp only [add_lie, map_add, h, h']; abel
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L),
    (S : (a : L) → L) ⁅y, z⁆ =
      HAdd.hAdd (β := L) (Bracket.bracket (L := L) ((S : (a : L) → L) y : L) z) (⁅y, (S : (a : L) → L) z⁆ : L)
⊢ ∀ (y z : L),
    (S : (a : L) → L) ⁅y, z⁆ = HSub.hSub (α := L) (β := L) (⁅y, (S : (a : L) → L) z⁆ : L) (⁅z, (S : (a : L) → L) y⁆ : L)

Tactic:
simp_rw [← lie_skew (S _) _, add_comm, ← sub_eq_add_neg] at h_der

Premises used: sub_eq_add_neg, add_comm, lie_skew, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
h_der :
  ∀ (y z : L),
    (S : (a : L) → L) ⁅y, z⁆ = HSub.hSub (α := L) (β := L) (⁅y, (S : (a : L) → L) z⁆ : L) (⁅z, (S : (a : L) → L) y⁆ : L)
⊢ ∀ (y z : L),
    (S : (a : L) → L) ⁅y, z⁆ = HSub.hSub (α := L) (β := L) (⁅y, (S : (a : L) → L) z⁆ : L) (⁅z, (S : (a : L) → L) y⁆ : L)

Tactic:
assumption