-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma restrict_killingForm_eq_sum :
    (killingForm K L).restrict H = ∑ α ∈ H.root, (α : H →ₗ[K] K).smulRight (α : H →ₗ[K] K)

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ ∈ LieSubalgebra.root
⊢ χ.IsNonZero

Tactic:
simpa [LieSubalgebra.root] using hχ

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ ∈ LieSubalgebra.root
⊢ finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)

Tactic:
replace hχ : χ.IsNonZero := by simpa [LieSubalgebra.root] using hχ

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ.IsNonZero
⊢ finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
⊢ (killingForm K L).restrict H.toSubmodule =
    ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)

Tactic:
rw [restrict_killingForm, traceForm_eq_sum_finrank_nsmul' K H L]

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
⊢ ∑ χ ∈ Finset.filter (fun χ => χ.IsNonZero) Finset.univ,
      finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ.IsNonZero
⊢ finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)

Tactic:
simp [finrank_rootSpace_eq_one _ hχ]

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
⊢ ∑ χ ∈ Finset.filter (fun χ => χ.IsNonZero) Finset.univ,
      finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)

Tactic:
refine Finset.sum_congr rfl fun χ hχ ↦ ?_

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ ∈ LieSubalgebra.root
⊢ finrank K ↥(genWeightSpace L ⇑χ) • (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)