-- Mathlib/Algebra/Lie/TraceForm.lean
lemma traceForm_eq_sum_finrank_nsmul_mul (x y : L) :
    traceForm K L M x y = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) • (χ x * χ y)

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace M ⇑i)
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
  ← traceForm_genWeightSpace_eq K L M _ x y]

Result:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace M ⇑i)
⊢ ∑ i : Weight K L M, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ x_1 : Weight K L M, ((traceForm K L ↥(genWeightSpace M ⇑x_1)) x) y

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
have hxy : ∀ χ : Weight K L M, MapsTo (toEnd K L M x ∘ₗ toEnd K L M y)
    (genWeightSpace M χ) (genWeightSpace M χ) :=
  fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm

Result:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace M ⇑i)
⊢ ∑ i : Weight K L M, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ x_1 : Weight K L M, ((traceForm K L ↥(genWeightSpace M ⇑x_1)) x) y

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  (LieSubmodule.iSupIndep_iff_toSubmodule.mp <| iSupIndep_genWeightSpace' K L M)
  (LieSubmodule.iSup_eq_top_iff_toSubmodule.mp <| iSup_genWeightSpace_eq_top' K L M)

Result:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace M ⇑i)
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
⊢ ((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
classical
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  (LieSubmodule.iSupIndep_iff_toSubmodule.mp <| iSupIndep_genWeightSpace' K L M)
  (LieSubmodule.iSup_eq_top_iff_toSubmodule.mp <| iSup_genWeightSpace_eq_top' K L M)
simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
  ← traceForm_genWeightSpace_eq K L M _ x y]
rfl

Result:
no goals