awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
Tactic: simp only [lie_add, map_add, h, h']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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 α
⊢ (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)
have 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)
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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
Tactic: simp only [add_lie, map_add, h, h']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
⊢ (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)
have 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)
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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
⊢ (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)
have 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)
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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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)
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have 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)
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
Cleared hypotheses: h_der
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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)
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have 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)
Tactic: replace h_der : ∀ y z : L, S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆ := by
    simp_rw [← lie_skew (S _) _, add_comm, ← sub_eq_add_neg] at h_der; assumption
Cleared hypotheses: h_der
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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)
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have obtain : ∀ (y : L) (hy : (LieDerivation.ad K L : (a : L) → LieDerivation K L L) y = S'),
  End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
Tactic: obtain ⟨y, hy⟩ := LieDerivation.IsKilling.exists_eq_ad S'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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)
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L : (a : L) → LieDerivation K L L) y = S'
z : L
hz : z ∈ H
⊢ ⁅y, z⁆ = 0
have hz₁ : z ∈ rootSpace H 0
Tactic: rw [← LieSubalgebra.mem_toLieSubmodule, ← rootSpace_zero_eq] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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)
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L : (a : L) → LieDerivation K L L) y = S'
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have hy' : ∀ (z : L) (hz : z ∈ H), ⁅y, z⁆ = 0
Tactic: have hy' (z : L) (hz : z ∈ H) : ⁅y, z⁆ = 0 := by
    rw [← LieSubalgebra.mem_toLieSubmodule, ← rootSpace_zero_eq] at hz
    simp [S', ← ad_apply (R := K), ← LieDerivation.coe_ad_apply_eq_ad_apply, hy, aux hz]