-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mapsTo_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) (k : ℕ∞) :
    MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k)

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
use l, hl

Result:
case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ((f - μ • 1) ^ l) (g x) = 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
⊢ MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)

Tactic:
intro x hx

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : x ∈ ↑((f.genEigenspace μ) k)
⊢ g x ∈ ↑((f.genEigenspace μ) k)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : x ∈ ↑((f.genEigenspace μ) k)
⊢ g x ∈ ↑((f.genEigenspace μ) k)

Tactic:
simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
  (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Proof state:
case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.mul_eq_comp, h.eq, LinearMap.mul_eq_comp,
  LinearMap.comp_apply, hx, map_zero]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
rcases hx with ⟨l, hl, hx⟩

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0