-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent. -/
lemma isNilpotent_restrict_genEigenspace_nat (f : End R M) (μ : R) (k : ℕ)
    (h : MapsTo (f - μ • (1 : End R M))
      (f.genEigenspace μ k) (f.genEigenspace μ k) :=
      mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ k) :
    IsNilpotent ((f - μ • 1).restrict h)

Proof state:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx : x ∈ (f.genEigenspace μ) ↑k
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
rw [mem_genEigenspace_nat] at hx

Result:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)

Proof state:
case h.h.mk.a.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ↑⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = ↑0

Tactic:
simpa

Result:
no goals

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
⊢ LinearMap.restrict (f - μ • 1) h ^ k = 0

Tactic:
ext ⟨x, hx⟩

Result:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx : x ∈ (f.genEigenspace μ) ↑k
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Proof state:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)

Tactic:
rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
  LinearMap.pow_restrict, LinearMap.restrict_apply]

Result:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0

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

Tactic:
use k

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
⊢ LinearMap.restrict (f - μ • 1) h ^ k = 0

Proof state:
case h.h.mk.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0

Tactic:
ext

Result:
case h.h.mk.a.a
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : optParam (MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ↑⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = ↑0