-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    iSupIndep (f.genEigenspace · k)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) (y + z) ∈ (f.genEigenspace μ₁) k ⊓ s.sup fun μ => (f.genEigenspace μ) k

Tactic:
refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩

Result:
case refine_1
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ Commute f (g ^ l)

case refine_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) (y + z) ∈ ↑(s.sup fun μ => (f.genEigenspace μ) k)

Proof state:
case refine_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) z ∈ s.sup fun μ => (f.genEigenspace μ) k

Tactic:
suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
    s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)

Result:
case refine_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ Submodule.map (g ^ l) (s.sup fun μ => (f.genEigenspace μ) k) ≤ s.sup fun μ => (f.genEigenspace μ) k