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
α : Weight K (↥H) L
⊢ Membership.mem (γ := Set (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (insert 0 (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
    (Weight.toLinear K (↥H) L α)
have simp : α.IsZero ∨ ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α
Tactic: simp only [mem_insert_iff, Weight.coe_toLinear_eq_zero_iff, mem_image, mem_setOf_eq]
-- 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
α : Weight K (↥H) L
⊢ α.IsZero ∨ ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α
have tauto : ¬α.IsZero → ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α
Tactic: tauto
-- 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
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (⨅ (α : Weight K (↥H) L), Weight.ker (M := L) (χ := α)) ⊥
have rw : Eq (α := Submodule K (Dual.{u_2, u_3} K ↥H))
  (⨆ (i : Weight K (↥H) L), Submodule.dualAnnihilator (Weight.ker (M := L) (χ := i))) ⊤
Tactic: rw [← Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq,
    Submodule.dualAnnihilator_bot]
-- 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
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have obtain : ∀ (N S : End K L) (hS₀ : Membership.mem (γ := Subalgebra K (End K L)) K[((ad K L : (a : L) → End K L) x : End K L)] S)
  (hN : _root_.IsNilpotent N) (hS : S.IsSemisimple) (hSN : (ad K L : (a : L) → End K L) x = N + S),
  End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
Tactic: obtain ⟨N, -, S, hS₀, hN, hS, hSN⟩ := (ad K L x).exists_isNilpotent_isSemisimple
-- 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
hS₀ : Membership.mem (γ := Subalgebra K (End K L)) K[((ad K L : (a : L) → End K L) x : End K L)] S
hN : _root_.IsNilpotent N
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have hS₁ : Commute ((ad K L : (a : L) → End K L) x) S
Tactic: replace hS₀ : Commute (ad K L x) S := Algebra.commute_of_mem_adjoin_self hS₀
Cleared hypotheses: hS₀
-- 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 N
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
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have hN₁ : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
Tactic: rw [eq_sub_of_add_eq hSN.symm] at hN
Cleared hypotheses: hN, hS, hSN, hS₀, x'
-- 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
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
⊢ (S : (a : L) → L) y = α x' • y
have hy₁ : Membership.mem (γ := Submodule K L) (maxGenEigenspace ((ad K L : (a : L) → End K L) x) (α x')) y
Tactic: replace hy : y ∈ (ad K L x).maxGenEigenspace (α x') :=
      (genWeightSpace_le_genWeightSpaceOf L x' α) hy
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
α : ↥H → K
y : L
hy : Membership.mem (γ := Submodule K L) (maxGenEigenspace ((ad K L : (a : L) → End K L) x) (α x')) y
⊢ (S : (a : L) → L) y = α x' • y
have hy₁ : Membership.mem (γ := Submodule K L)
  ((genEigenspace ((ad K L : (a : L) → End K L) x) (α x') : (a : ℕ∞) → Submodule K L)
      (↑(maxGenEigenspaceIndex.{u_2, u_3} (M := L) ((ad K L : (a : L) → End K L) x) (α x')) : ℕ∞) :
    Submodule K L)
  y
Tactic: rw [maxGenEigenspace_eq] at hy
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
α : ↥H → K
y : L
k : ℕ := maxGenEigenspaceIndex.{u_2, u_3} (M := L) ((ad K L : (a : L) → End K L) x) (α x')
hy :
  Membership.mem (γ := Submodule K L)
    ((genEigenspace ((ad K L : (a : L) → End K L) x) (α x') : (a : ℕ∞) → Submodule K L) (↑k : ℕ∞) : Submodule K L) y
⊢ (S : (a : L) → L) y = α x' • y
have rw : α x' • y = α x' • y
Tactic: rw [apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hy hS₀ hS.isFinitelySemisimple hN]
-- 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
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
Tactic: have aux {α : H → K} {y : L} (hy : y ∈ rootSpace H α) : S y = α x' • y := by
    replace hy : y ∈ (ad K L x).maxGenEigenspace (α x') :=
      (genWeightSpace_le_genWeightSpaceOf L x' α) hy
    rw [maxGenEigenspace_eq] at hy
    set k := maxGenEigenspaceIndex (ad K L x) (α x')
    rw [apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hy hS₀ hS.isFinitelySemisimple hN]
-- 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
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)
have hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
Tactic: have hyz : ⁅y, z⁆ ∈ rootSpace H (α + β) :=
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α β hy 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, 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)
have rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, 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 rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • 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 rw₂ : (α + β) x' • ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₂ : (α + β) x' • ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • 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 rw₃ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + ⁅y, β x' • z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₂ : (α + β) x' • ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₃ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + ⁅y, β x' • 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 rw₄ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + β x' • ⁅y, z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₂ : (α + β) x' • ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₃ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + ⁅y, β x' • z⁆
rw₄ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + β x' • ⁅y, 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 rw₅ : (α + β) x' • ⁅y, z⁆ = (α x' + β x') • ⁅y, z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
rw : (S : (a : L) → L) ⁅y, z⁆ = HAdd.hAdd (β := L) ⁅α x' • y, z⁆ (⁅y, (S : (a : L) → L) z⁆ : L)
rw₁ : (S : (a : L) → L) ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₂ : (α + β) x' • ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆
rw₃ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + ⁅y, β x' • z⁆
rw₄ : (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + β x' • ⁅y, z⁆
rw₅ : (α + β) x' • ⁅y, z⁆ = (α x' + β x') • ⁅y, 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 rw₆ : (α + β) x' • ⁅y, z⁆ = (α + β) x' • ⁅y, z⁆
Tactic: rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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
⊢ 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) (α β : ↥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)
Tactic: have h_der (y z : L) (α β : H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β) :
      S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆ := by
    have hyz : ⁅y, z⁆ ∈ rootSpace H (α + β) :=
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α β hy hz
    rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]
-- 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)
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)
have hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) y
Tactic: have hy : y ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_genWeightSpace_eq_top]
-- 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)
y z : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (α : ↥H → K), rootSpace H α) y
⊢ (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 hz : 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]