-- Mathlib/Algebra/Lie/TraceForm.lean
lemma traceForm_eq_sum_genWeightSpaceOf
    [NoZeroSMulDivisors R M] [IsNoetherian R M] [IsTriangularizable R L M] (z : L) :
    traceForm R L M =
    ∑ χ ∈ (finite_genWeightSpaceOf_ne_bot R L M z).toFinset,
      traceForm R L (genWeightSpaceOf M χ z)

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Tactic:
have hfin : {χ : R | (genWeightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
  convert finite_genWeightSpaceOf_ne_bot R L M z
  exact LieSubmodule.toSubmodule_eq_bot (genWeightSpaceOf M _ _)

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z : L
⊢ traceForm R L M = ∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)

Tactic:
ext x y

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
⊢ ((traceForm R L M) x) y = ((∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)) x) y

Tactic:
classical
have h := LieSubmodule.iSupIndep_iff_toSubmodule.mp <| iSupIndep_genWeightSpaceOf R L M z
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
  simp [← LieSubmodule.iSup_toSubmodule]
simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
  LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
h : iSupIndep fun i => ↑(genWeightSpaceOf M i z)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpaceOf M i z)
⊢ hfin.toFinset = ⋯.toFinset

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
h : iSupIndep fun i => ↑(genWeightSpaceOf M i z)
⊢ ⨆ i, ↑(genWeightSpaceOf M i z) = ⊤

Tactic:
simp [← LieSubmodule.iSup_toSubmodule]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
⊢ {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite

Tactic:
convert finite_genWeightSpaceOf_ne_bot R L M z

Result:
case h.e'_2.h.e'_2.h.h.a
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
x✝ : R
⊢ ↑(genWeightSpaceOf M x✝ z) = ⊥ ↔ genWeightSpaceOf M x✝ z = ⊥

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z x y : L
hxy : ∀ (χ : R), MapsTo ⇑(φ x ∘ₗ φ y) ↑(genWeightSpaceOf M χ z) ↑(genWeightSpaceOf M χ z)
hfin : {χ | ↑(genWeightSpaceOf M χ z) ≠ ⊥}.Finite
h : iSupIndep fun i => ↑(genWeightSpaceOf M i z)
hds : DirectSum.IsInternal fun i => ↑(genWeightSpaceOf M i z)
⊢ ∑ i ∈ hfin.toFinset, (trace R ↥↑(genWeightSpaceOf M i z)) ((φ x ∘ₗ φ y).restrict ⋯) =
    ∑ x_1 ∈ ⋯.toFinset,
      (trace R ↥(genWeightSpaceOf M x_1 z))
        ((toEnd R L ↥(genWeightSpaceOf M x_1 z)) x ∘ₗ (toEnd R L ↥(genWeightSpaceOf M x_1 z)) y)

Tactic:
exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)

Result:
no goals