-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for positive exponents. -/
lemma HasUnifEigenvalue.lt {f : End R M} {μ : R} {k m : ℕ∞}
    (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) :
    f.HasUnifEigenvalue μ m

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ False

Tactic:
apply hk

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (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 : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : x ∈ (f.genEigenspace μ) k
⊢ x ∈ ⊥

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ Function.Injective (⇑(f - μ • 1))^[l]

Tactic:
exact Function.Injective.iterate contra l

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ 1

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ 1

Tactic:
intro contra

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ False

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ x ∈ ⊥

Tactic:
rwa [LinearMap.ker_eq_bot.mpr] at hx

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ Function.Injective ⇑((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 m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : ∃ l, ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ x ∈ ⊥

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

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ 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 m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (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 : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ Function.Injective ⇑((f - μ • 1) ^ l)

Tactic:
rw [LinearMap.coe_pow (f - μ • 1) l]

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ Function.Injective (⇑(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 m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : x ∈ (f.genEigenspace μ) k
⊢ x ∈ ⊥

Tactic:
rw [mem_genEigenspace] at hx

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : ∃ l, ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)
⊢ 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 m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k ≤ ⊥