-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenrange_nat {f : End R M} {μ : R} {k : ℕ} :
    f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k)

Proof state:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ k) x

Tactic:
rw [this, pow_add]

Result:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ i * (f - μ • 1) ^ (k - i)) x

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 : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) ↔ ∃ y, ((f - μ • 1) ^ k) y = x

Tactic:
constructor

Result:
case h.mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x

case h.mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Proof state:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ i * (f - μ • 1) ^ (k - i)) x

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case h.mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x

Tactic:
intro h

Result:
case h.mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
h : ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x
⊢ ∃ y, ((f - μ • 1) ^ k) y = x

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ k = i + (k - i)

Tactic:
omega

Result:
no goals

Proof state:
case h.mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
h : ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x
⊢ ∃ y, ((f - μ • 1) ^ k) y = x

Tactic:
exact h _ le_rfl

Result:
no goals

Proof state:
case h.mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
rintro ⟨x, rfl⟩ i hi

Result:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ k) x

Proof state:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ k) x

Tactic:
have : k = i + (k - i) := by omega

Result:
case h.mpr.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ k) x

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 : ℕ
x : M
⊢ x ∈ f.genEigenrange μ ↑k ↔ x ∈ LinearMap.range ((f - μ • 1) ^ k)

Tactic:
simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]

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 : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) ↔ ∃ y, ((f - μ • 1) ^ k) y = x

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
⊢ f.genEigenrange μ ↑k = LinearMap.range ((f - μ • 1) ^ k)

Tactic:
ext x

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 : ℕ
x : M
⊢ x ∈ f.genEigenrange μ ↑k ↔ x ∈ LinearMap.range ((f - μ • 1) ^ k)