-- Mathlib/Algebra/DirectSum/LinearMap.lean
/-- If `f` and `g` are commuting endomorphisms of a finite, free `R`-module `M`, such that `f`
is triangularizable, then to prove that the trace of `g ∘ f` vanishes, it is sufficient to prove
that the trace of `g` vanishes on each generalized eigenspace of `f`. -/
lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
    [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
    {f g : Module.End R M}
    (h_comm : Commute f g)
    (hf : ⨆ μ, f.maxGenEigenspace μ = ⊤)
    (hg : ∀ μ, trace R _ (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ)) = 0) :
    trace R _ (g ∘ₗ f) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
rw [restrict_comp, trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm
  (f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ), hg, mul_zero]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
  WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite
⊢ (trace R M) (g ∘ₗ f) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
intro μ

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have hfg : ∀ μ,
    MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
  fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
    (f.mapsTo_maxGenEigenspace_of_comm rfl μ)

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R M) (g ∘ₗ f) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
  classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    f.independent_maxGenEigenspace hf
  have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
    WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
  simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
classical
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  f.independent_maxGenEigenspace hf
have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
  WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]

Result:
no goals