-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma maxUnifEigenspaceIndex_le_finrank [FiniteDimensional K V] (f : End K V) (μ : K) :
    maxUnifEigenspaceIndex f μ ≤ finrank K V

Proof state:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V)

Tactic:
show (f.genEigenspace μ) n ≤ (f.genEigenspace μ) (finrank K V)

Result:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ (f.genEigenspace μ) ↑n ≤ (f.genEigenspace μ) ↑(finrank K V)

Proof state:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ LinearMap.ker ((f - μ • 1) ^ n) ≤ LinearMap.ker ((f - μ • 1) ^ finrank K V)

Tactic:
apply ker_pow_le_ker_pow_finrank

Result:
no goals

Proof state:
case hm
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Tactic:
apply le_antisymm

Result:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V)

Proof state:
case hm
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ∈
    {n |
      ∀ (m : ℕ),
        n ≤ m →
          ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n =
            ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) m}

Tactic:
intro n hn

Result:
case hm
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Proof state:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ (f.genEigenspace μ) ↑n ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_nat, genEigenspace_nat]

Result:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ LinearMap.ker ((f - μ • 1) ^ n) ≤ LinearMap.ker ((f - μ • 1) ^ finrank K V)

Proof state:
case hm.a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Tactic:
exact (f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ f.maxUnifEigenspaceIndex μ ≤ finrank K V

Tactic:
apply Nat.sInf_le

Result:
case hm
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ∈
    {n |
      ∀ (m : ℕ),
        n ≤ m →
          ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n =
            ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) m}