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),
    (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:
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
-- 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)
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
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)
⊢ 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'

Premises used: LieDerivation.IsKilling.exists_eq_ad
-- 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)
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
⊢ z ∈ rootSpace H 0

Tactic:
rw [← LieSubalgebra.mem_toLieSubmodule, ← rootSpace_zero_eq] at hz

Premises used: LieSubalgebra.mem_toLieSubmodule, LieAlgebra.rootSpace_zero_eq
-- 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)
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 ∈ rootSpace H 0
⊢ ⁅y, z⁆ = 0

Tactic:
simp [S', ← ad_apply (R := K), ← LieDerivation.coe_ad_apply_eq_ad_apply, hy, aux hz]

Premises used: LieAlgebra.ad_apply, LieDerivation.coe_ad_apply_eq_ad_apply
-- 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)
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

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]
-- 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)
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : y ∈ H), y ∈ H
⊢ y ∈ H

Tactic:
rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this

Premises used: LieSubalgebra.IsCartanSubalgebra.self_normalizing
-- 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)
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
suffices : y ∈ H.normalizer
⊢ y ∈ H

Tactic:
suffices y ∈ H.normalizer by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this
-- 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)
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.normalizer

Tactic:
(H.mem_normalizer_iff y).mpr fun z hz ↦ hy' z hz ▸ LieSubalgebra.zero_mem H

Premises used: Iff.mpr, Eq.rec, LieSubalgebra.zero_mem, Eq.symm, LieSubalgebra.mem_normalizer_iff
-- 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)
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.normalizer

Tactic:
exact (H.mem_normalizer_iff y).mpr fun z hz ↦ hy' z hz ▸ LieSubalgebra.zero_mem H

Premises used: Iff.mpr, Eq.rec, LieSubalgebra.zero_mem, Eq.symm, LieSubalgebra.mem_normalizer_iff
-- 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)
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

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
-- 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)
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)
rwa₂ rwa₃ rwa₄ rwa₅ : End.IsSemisimple (↑S' : L →ₗ[K] L)
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)

Tactic:
rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, hy]

Premises used: LieDerivation.coe_ad_apply_eq_ad_apply
-- 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)
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
suffices : x = y
⊢ End.IsSemisimple.{u_2, u_3} (R := K) (M := L) ((ad K L : (a : L) → End K L) x)

Tactic:
suffices x = y by rwa [this, ← LieDerivation.coe_ad_apply_eq_ad_apply y, hy]
-- 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)
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 : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- 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)
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
apply : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)
⊢ x - y = 0

Tactic:
apply eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra K L H (H.sub_mem hx hy')

Premises used: LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra, LieSubalgebra.sub_mem
-- 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)
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)
rw₁ rw₂ : S = (↑S' : L →ₗ[K] L)
⊢ S = (ad K L : (a : L) → End K L) y

Tactic:
rw [← LieDerivation.coe_ad_apply_eq_ad_apply y, hy]

Premises used: LieDerivation.coe_ad_apply_eq_ad_apply
-- 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)
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

Tactic:
replace hy : S = ad K L y := by rw [← LieDerivation.coe_ad_apply_eq_ad_apply y, hy]
-- 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)
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))
rwa₃ : _root_.IsNilpotent N
rwa₄ rwa₅ rwa₆ rwa₇ : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
⊢ _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) (x - y) : End K L)

Tactic:
rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.symm]

Premises used: map_sub, eq_sub_of_add_eq, add_sub_cancel_right, Eq.symm
-- 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
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
h : ↥H
⊢ 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
-- 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
α : ↥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
⊢ (((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

Premises used: Module.End.mem_eigenspace_iff, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, Module.End.IsSemisimple.isFinitelySemisimple, Subtype.property, Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace
-- 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
α : ↥H → K
x : L
h : ↥H
hx : (((ad K L : (a : L) → End K L) (↑h : L) : End K L) : (a : L) → L) x = α h • x
⊢ ⁅h, x⁆ = α h • x

Tactic:
simpa using hx
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
apply : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
⊢ ⁅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)

Tactic:
apply lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα

Premises used: LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux