-- Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean
lemma apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil
    {μ : R} {k : ℕ∞} {m : M} (hm : m ∈ f.genEigenspace μ k)
    (hfg : Commute f g) (hss : g.IsFinitelySemisimple) (hnil : IsNilpotent (f - g)) :
    g m = μ • m

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
⊢ g m = μ • m

Tactic:
suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by
  replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
    eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
  simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
⊢ IsNilpotent (LinearMap.restrict (g - (algebraMap R (End R M)) μ) h₂)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ LinearMap.ker ((f - μ • 1) ^ l)
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
obtain ⟨l, -, hm⟩ := hm

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : m ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ g m = μ • m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
rw [f.mem_genEigenspace] at hm

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ LinearMap.ker ((f - μ • 1) ^ l)
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : m ∈ (f.genEigenspace μ) ↑l
⊢ g m = μ • m

Tactic:
set p := f.genEigenspace μ l

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
⊢ g m = μ • m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
this : IsNilpotent (LinearMap.restrict (g - (algebraMap R (End R M)) μ) h₂)
⊢ g m = μ • m

Tactic:
replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
  eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
this : LinearMap.restrict g h₁ - (algebraMap R (End R ↥p)) μ = 0
⊢ g m = μ • m