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),
    (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'
hy' : ∀ (z : L) (hz : z ∈ H), ⁅y, z⁆ = 0
this : y ∈ H.normalizer
⊢ y ∈ H
have rwa : ∀ (this : y ∈ H), y ∈ H
Tactic: rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this
Cleared hypotheses: this
-- 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 }
y : L
hy : (LieDerivation.ad K L : (a : L) → LieDerivation K L L) y = S'
hy' : ∀ (z : L) (hz : z ∈ H), ⁅y, z⁆ = 0
⊢ y ∈ H
have suffices : y ∈ H.normalizer
Tactic: suffices y ∈ H.normalizer by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this
-- 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'
hy' : ∀ (z : L) (hz : z ∈ H), ⁅y, z⁆ = 0
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have hy'₁ : y ∈ H
Tactic: replace hy' : y ∈ H := by
    suffices y ∈ H.normalizer by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this
    exact (H.mem_normalizer_iff y).mpr fun z hz ↦ hy' z hz ▸ LieSubalgebra.zero_mem H
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),
    (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'
hy' : y ∈ H
this : x = y
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have rwa : End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) y)
Tactic: rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
this : x = y
rwa : End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) y)
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have rwa₁ : End.IsSemisimple.{u_2, u_3} (R := K) (M := L) (↑((LieDerivation.ad K L : (a : L) → LieDerivation K L L) y) : L →ₗ[K] L)
Tactic: rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
this : x = y
rwa : End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) y)
rwa₁ :
  End.IsSemisimple.{u_2, u_3} (R := K) (M := L)
    (↑((LieDerivation.ad K L : (a : L) → LieDerivation K L L) y) : L →ₗ[K] L)
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have rwa₂ : End.IsSemisimple (↑S' : L →ₗ[K] L)
Tactic: rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)
have suffices : x = y
Tactic: suffices x = y by rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- 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 }
y : L
hy : (LieDerivation.ad K L : (a : L) → LieDerivation K L L) y = S'
hy' : y ∈ H
⊢ x - y = 0
have apply : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
Tactic: apply eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra K L H (H.sub_mem hx 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),
    (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'
hy' : y ∈ H
⊢ S = (ad K L : (a : L) → End K L) y
have rw : S = (↑((LieDerivation.ad K L : (a : L) → LieDerivation K L L) y) : L →ₗ[K] L)
Tactic: rw [← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
rw : S = (↑((LieDerivation.ad K L : (a : L) → LieDerivation K L L) y) : L →ₗ[K] L)
⊢ S = (ad K L : (a : L) → End K L) y
have rw₁ : S = (↑S' : L →ₗ[K] L)
Tactic: rw [← LieDerivation.coe_ad_apply_eq_ad_apply y, 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),
    (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'
hy' : y ∈ H
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
have hy₁ : S = (ad K L : (a : L) → End K L) y
Tactic: replace hy : S = ad K L y := by rw [← LieDerivation.coe_ad_apply_eq_ad_apply y, 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
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' : y ∈ H
hy : S = (ad K L : (a : L) → End K L) y
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
have rwa : _root_.IsNilpotent
  (HSub.hSub (α := End K L) (β := End K L) ((ad K L : (a : L) → End K L) x : End K L)
    ((ad K L : (a : L) → End K L) y : End K L))
Tactic: rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.symm]
-- 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 }
y : L
hy' : y ∈ H
hy : S = (ad K L : (a : L) → End K L) y
rwa :
  _root_.IsNilpotent
    (HSub.hSub (α := End K L) (β := End K L) ((ad K L : (a : L) → End K L) x : End K L)
      ((ad K L : (a : L) → End K L) y : End K L))
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
have rwa₁ : _root_.IsNilpotent (HSub.hSub (β := End K L) (N + S) ((ad K L : (a : L) → End K L) y : End K L))
Tactic: rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.symm]
-- 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 }
y : L
hy' : y ∈ H
hy : S = (ad K L : (a : L) → End K L) y
rwa :
  _root_.IsNilpotent
    (HSub.hSub (α := End K L) (β := End K L) ((ad K L : (a : L) → End K L) x : End K L)
      ((ad K L : (a : L) → End K L) y : End K L))
rwa₁ : _root_.IsNilpotent (HSub.hSub (β := End K L) (N + S) ((ad K L : (a : L) → End K L) y : End K L))
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
have rwa₂ : _root_.IsNilpotent
  (HSub.hSub (β := End K L) (HAdd.hAdd (β := End K L) N ((ad K L : (a : L) → End K L) y : End K L))
    ((ad K L : (a : L) → End K L) y : End K L))
Tactic: rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.symm]
-- 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 }
y : L
hy' : y ∈ H
hy : S = (ad K L : (a : L) → End K L) y
rwa :
  _root_.IsNilpotent
    (HSub.hSub (α := End K L) (β := End K L) ((ad K L : (a : L) → End K L) x : End K L)
      ((ad K L : (a : L) → End K L) y : End K L))
rwa₁ : _root_.IsNilpotent (HSub.hSub (β := End K L) (N + S) ((ad K L : (a : L) → End K L) y : End K L))
rwa₂ :
  _root_.IsNilpotent
    (HSub.hSub (β := End K L) (HAdd.hAdd (β := End K L) N ((ad K L : (a : L) → End K L) y : End K L))
      ((ad K L : (a : L) → End K L) y : End K L))
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
have rwa₃ : _root_.IsNilpotent N
Tactic: rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.symm]
-- 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
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
h : ↥H
⊢ ⁅h, x⁆ = α h • x
have hx₁ : Membership.mem (γ := Submodule K L) (End.maxGenEigenspace ((ad K L : (a : L) → End K L) (↑h : L)) (α h)) x
Tactic: replace hx : x ∈ (ad K L h).maxGenEigenspace (α h) :=
    genWeightSpace_le_genWeightSpaceOf L h α hx
Cleared hypotheses: hx
-- 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
α : ↥H → K
x : L
h : ↥H
hx : Membership.mem (γ := Submodule K L) (End.maxGenEigenspace ((ad K L : (a : L) → End K L) (↑h : L)) (α h)) x
⊢ ⁅h, x⁆ = α h • x
have hx₁ : (((ad K L : (a : L) → End K L) (↑h : L) : End K L) : (a : L) → L) x = α h • x
Tactic: rw [(isSemisimple_ad_of_mem_isCartanSubalgebra
    h.property).isFinitelySemisimple.maxGenEigenspace_eq_eigenspace,
    Module.End.mem_eigenspace_iff] at hx
Cleared hypotheses: hx
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
have apply : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
Tactic: apply lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα
-- 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
α : Weight K (↥H) L
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
have refine_1 : LE.le (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
  (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
Tactic: refine le_antisymm ?_ ?_