-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mem_genEigenspace_nat {f : End R M} {μ : R} {k : ℕ} {x : M} :
    x ∈ f.genEigenspace μ k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
case 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
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Tactic:
exact ⟨k, le_rfl, hx⟩

Result:
no goals

Proof state:
case mp.intro.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
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
hl : l ≤ k
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
exact (f - μ • 1).iterateKer.monotone hl hx

Result:
no goals

Proof state:
case 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
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k) → ∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Tactic:
intro hx

Result:
case 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
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ k)
⊢ ∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

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
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)) ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
constructor

Result:
case 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
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)) → x ∈ LinearMap.ker ((f - μ • 1) ^ k)

case 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
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k) → ∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

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
⊢ x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
rw [mem_genEigenspace]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)) ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
case mp.intro.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
l : ℕ
hl : ↑l ≤ ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
simp only [Nat.cast_le] at hl

Result:
case mp.intro.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
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
hl : l ≤ k
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
case 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
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)) → x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
rintro ⟨l, hl, hx⟩

Result:
case mp.intro.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
l : ℕ
hl : ↑l ≤ ↑k
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ x ∈ LinearMap.ker ((f - μ • 1) ^ k)