-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent. -/
@[deprecated isNilpotent_restrict_maxGenEigenspace_sub_algebraMap (since := "2024-10-23")]
lemma isNilpotent_restrict_iSup_sub_algebraMap [IsNoetherian R M] (f : End R M) (μ : R)
    (h : MapsTo (f - algebraMap R (End R M) μ)
      ↑(⨆ k : ℕ, f.genEigenspace μ k) ↑(⨆ k : ℕ, f.genEigenspace μ k) :=
      mapsTo_iSup_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ) :
    IsNilpotent ((f - algebraMap R (End R M) μ).restrict h)

Proof state:
case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
⊢ ∀ (i : ℕ), (f.genEigenspace μ) ↑i ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
intro k

Result:
case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
k : ℕ
⊢ (f.genEigenspace μ) ↑k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
⊢ ⨆ k, (f.genEigenspace μ) ↑k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
apply iSup_le

Result:
case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
⊢ ∀ (i : ℕ), (f.genEigenspace μ) ↑i ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Proof state:
case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
k : ℕ
⊢ (f.genEigenspace μ) ↑k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
apply genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)

Tactic:
apply isNilpotent_restrict_of_le (q := f.genEigenspace μ (maxUnifEigenspaceIndex f μ))
  _ (isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ))

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)) ⋯
⊢ ⨆ k, (f.genEigenspace μ) ↑k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)