[GOAL]
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, HasEigenvalue f c
[PROOFSTEP]
simp_rw [hasEigenvalue_iff_mem_spectrum]
[GOAL]
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f
[PROOFSTEP]
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f
[GOAL]
K : Type v
V : Type w
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
induction' h_dim : finrank K V using Nat.strong_induction_on with n ih generalizing V
[GOAL]
case h
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_dim : finrank K V = n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.zero
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
rw [← top_le_iff]
[GOAL]
case h.zero
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.zero
⊢ ⊤ ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
simp only [finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]
  -- Otherwise the vector space is nontrivial.
[GOAL]
case h.succ
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
haveI : Nontrivial V :=
  finrank_pos_iff.1
    (by rw [h_dim]; apply Nat.zero_lt_succ)
      -- Hence, `f` has an eigenvalue `μ₀`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ 0 < finrank ?m.10065 V
[PROOFSTEP]
rw [h_dim]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
apply Nat.zero_lt_succ
[GOAL]
case h.succ
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let ES :=
  f.generalizedEigenspace μ₀
    (finrank K V)
      -- and `ER` to be the generalized eigenrange.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let ER :=
  f.generalizedEigenrange μ₀
    (finrank K V)
      -- `f` maps `ER` into itself.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_f_ER : ∀ x : V, x ∈ ER → f x ∈ ER := fun x hx =>
  map_generalizedEigenrange_le
    (Submodule.mem_map_of_mem hx)
      -- Therefore, we can define the restriction `f'` of `f` to `ER`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let f' : End K ER := f.restrict h_f_ER
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_ES_pos : 0 < finrank K ES := by
  dsimp only
  rw [h_dim]
  apply
    pos_finrank_generalizedEigenspace_of_hasEigenvalue hμ₀
      (Nat.zero_lt_succ n)
        -- and the dimensions of `ES` and `ER` add up to `finrank K V`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ES }
[PROOFSTEP]
dsimp only
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ↑(generalizedEigenspace f μ₀) (finrank K V) }
[PROOFSTEP]
rw [h_dim]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ↑(generalizedEigenspace f μ₀) (Nat.succ n) }
[PROOFSTEP]
apply
  pos_finrank_generalizedEigenspace_of_hasEigenvalue hμ₀
    (Nat.zero_lt_succ n)
      -- and the dimensions of `ES` and `ER` add up to `finrank K V`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_add : finrank K ER + finrank K ES = finrank K V := by apply LinearMap.finrank_range_add_finrank_ker
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
⊢ finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
[PROOFSTEP]
apply LinearMap.finrank_range_add_finrank_ker
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_ER : finrank K ER < n.succ := by
  linarith
    -- This allows us to apply the induction hypothesis on `ER`:
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
⊢ finrank K { x // x ∈ ER } < Nat.succ n
[PROOFSTEP]
linarith
  -- This allows us to apply the induction hypothesis on `ER`:
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have ih_ER : ⨆ (μ : K) (k : ℕ), f'.generalizedEigenspace μ k = ⊤ := ih (finrank K ER) h_dim_ER f' rfl
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have ih_ER' : ⨆ (μ : K) (k : ℕ), (f'.generalizedEigenspace μ k).map ER.subtype = ER := by
  simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
    -- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized
        -- eigenspace of `f`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
⊢ ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
[PROOFSTEP]
simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
  -- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized
      -- eigenspace of `f`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hff' : ∀ μ k, (f'.generalizedEigenspace μ k).map ER.subtype ≤ f.generalizedEigenspace μ k :=
  by
  intros
  rw [generalizedEigenspace_restrict]
  apply Submodule.map_comap_le
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
⊢ ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
intros
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
μ✝ : K
k✝ : ℕ
⊢ Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ✝) k✝) ≤ ↑(generalizedEigenspace f μ✝) k✝
[PROOFSTEP]
rw [generalizedEigenspace_restrict]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
μ✝ : K
k✝ : ℕ
⊢ Submodule.map (Submodule.subtype ER) (Submodule.comap (Submodule.subtype ER) (↑(generalizedEigenspace f μ✝) k✝)) ≤
    ↑(generalizedEigenspace f μ✝) k✝
[PROOFSTEP]
apply Submodule.map_comap_le
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hER : ER ≤ ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k :=
  by
  rw [← ih_ER']
  exact iSup₂_mono hff'
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
rw [← ih_ER']
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤
    ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
exact iSup₂_mono hff'
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hES : ES ≤ ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k :=
  le_trans (le_iSup (fun k => f.generalizedEigenspace μ₀ k) (finrank K V))
    (le_iSup (fun μ : K => ⨆ k : ℕ, f.generalizedEigenspace μ k) μ₀)
      -- Moreover, we know that `ER` and `ES` are disjoint.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
show ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k = ⊤
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint]
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ER ⊔ ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
apply sup_le hER hES
