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
rw :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (LinearMap.flip (traceForm K (↥H) L)))
rw₁ :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (Submodule.dualAnnihilator (LinearMap.ker (traceForm K (↥H) L)))
rw₂ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ (Submodule.dualAnnihilator ⊥)
rw₃ rw₄ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ ⊤
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))

Tactic:
rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]

Premises used: LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, Membership.mem, Subtype, Submodule.dualAnnihilator_bot, LieModule.traceForm_flip, LinearMap.dualAnnihilator_ker_eq_range_flip
-- 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
rw :
  Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})) ⊤

Tactic:
rw [← span_weight_eq_top]

Premises used: LieAlgebra.IsKilling.span_weight_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
⊢ Subset (α := Set (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})
    (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
refine :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))

Tactic:
refine le_antisymm (Submodule.span_mono <| by simp) ?_

Premises used: le_antisymm, Submodule.span_mono
-- 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
this :
  Subset (α := Set (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))
    (insert 0 (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))

Tactic:
simpa only [Submodule.span_insert_zero] using Submodule.span_mono this

Premises used: Submodule.span_mono, Submodule.span_insert_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
suffices :
  Subset (α := Set (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))
    (insert 0 (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))

Tactic:
suffices range (Weight.toLinear K H L) ⊆
    insert 0 ({α : Weight K H L | α.IsNonZero}.image (Weight.toLinear K H L)) by
    simpa only [Submodule.span_insert_zero] using Submodule.span_mono 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
α : Weight K (↥H) L
simp : α.IsZero ∨ ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear 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 α)

Tactic:
simp only [mem_insert_iff, Weight.coe_toLinear_eq_zero_iff, mem_image, mem_setOf_eq]

Premises used: Set.mem_image, LieModule.Weight.coe_toLinear_eq_zero_iff, Set.mem_setOf_eq, Set.mem_insert_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
α : Weight K (↥H) L
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ :
  ¬α.IsZero → ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α
⊢ α.IsZero ∨ ∃ (x : Weight K (↥H) L), x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α

Tactic:
tauto
-- 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
rw :
  Eq (α := Submodule K (Dual.{u_2, u_3} K ↥H))
    (⨆ (i : Weight K (↥H) L), Submodule.dualAnnihilator (Weight.ker (M := L) (χ := i))) ⊤
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (⨅ (α : Weight K (↥H) L), Weight.ker (M := L) (χ := α)) ⊥

Tactic:
rw [← Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq,
    Submodule.dualAnnihilator_bot]

Premises used: Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq, Submodule.dualAnnihilator_bot
-- 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
⊢ Eq (α := Submodule K (Dual.{u_2, u_3} K ↥H))
    (⨆ (i : Weight K (↥H) L), Submodule.dualAnnihilator (Weight.ker (M := L) (χ := i))) ⊤

Tactic:
simp [← LinearMap.range_dualMap_eq_dualAnnihilator_ker, ← Submodule.span_range_eq_iSup]

Premises used: Submodule.span_range_eq_iSup, LinearMap.range_dualMap_eq_dualAnnihilator_ker
-- 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
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)
⊢ 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

Premises used: Module.End.exists_isNilpotent_isSemisimple
-- 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
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
⊢ 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₀
-- 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 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
⊢ _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

Premises used: eq_sub_of_add_eq, 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
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
hN₁ : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
⊢ S.IsSemisimple

Tactic:
rw [eq_sub_of_add_eq hSN.symm] at hN

Premises used: eq_sub_of_add_eq, 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
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
hN₁ : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS₁ : S.IsSemisimple
⊢ (ad K L : (a : L) → End K L) x = N + S

Tactic:
rw [eq_sub_of_add_eq hSN.symm] at hN

Premises used: eq_sub_of_add_eq, 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
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
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
⊢ Commute ((ad K L : (a : L) → End K L) x) S

Tactic:
rw [eq_sub_of_add_eq hSN.symm] at hN

Premises used: eq_sub_of_add_eq, 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
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 α
⊢ 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
-- 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
α : ↥H → K
y : L
hy : Membership.mem (γ := Submodule K L) (maxGenEigenspace ((ad K L : (a : L) → End K L) x) (α x')) y
⊢ 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

Premises used: Module.End.maxGenEigenspace_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
α : ↥H → K
y : L
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
⊢ let k := maxGenEigenspaceIndex.{u_2, u_3} (M := L) ((ad K L : (a : L) → End K L) x) (α x');
  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

Tactic:
set k := maxGenEigenspaceIndex (ad K L x) (α x')

Premises used: Module.End.maxGenEigenspaceIndex, LieAlgebra.ad, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
α : ↥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
rw rw₁ : α x' • y = α x' • y
⊢ (S : (a : L) → L) y = α x' • y

Tactic:
rw [apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hy hS₀ hS.isFinitelySemisimple hN]

Premises used: Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil, Module.End.IsSemisimple.isFinitelySemisimple
-- 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
⊢ ∀ {α : ↥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]
-- 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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
⊢ ⁅y, z⁆ ∈ rootSpace H (α + β)

Tactic:
have hyz : ⁅y, z⁆ ∈ rootSpace H (α + β) :=
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α β hy hz
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent (HSub.hSub (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) S)
hS : S.IsSemisimple
hSN : (ad K L : (a : L) → End K L) x = N + S
hS₀ : Commute ((ad K L : (a : L) → End K L) x) S
x' : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
aux : ∀ {α : ↥H → K} {y : L} (hy : y ∈ rootSpace H α), (S : (a : L) → L) y = α x' • y
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⁆
rw₆ rw₇ : (α + β) 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)

Tactic:
rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]

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

Tactic:
simp [iSup_genWeightSpace_eq_top]

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