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) = ⊤
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) = ⊤
induction' h_dim : finrank K V using Nat.strong_induction_on with n ih generalizing V
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) = ⊤

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) = ⊤
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) = ⊤
cases' n with n
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
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) = ⊤
rw [← top_le_iff]
no goals
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
simp only [finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]
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) = ⊤
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) = ⊤
haveI : Nontrivial V := finrank_pos_iff.1 (by rw [h_dim]; apply Nat.zero_lt_succ)
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) = ⊤
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) = ⊤
obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f
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) = ⊤
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) = ⊤
let ES := f.generalizedEigenspace μ₀ (finrank K V)
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) = ⊤
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) = ⊤
let ER := f.generalizedEigenrange μ₀ (finrank K V)
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) = ⊤
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) = ⊤
have h_f_ER : ∀ x : V, x ∈ ER → f x ∈ ER := fun x hx =>
  map_generalizedEigenrange_le (Submodule.mem_map_of_mem hx)
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) = ⊤
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) = ⊤
let f' : End K ER := f.restrict h_f_ER
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) = ⊤
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) = ⊤
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)
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) = ⊤
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) = ⊤
have h_dim_add : finrank K ER + finrank K ES = finrank K V := by
  apply LinearMap.finrank_range_add_finrank_ker
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) = ⊤
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) = ⊤
have h_dim_ER : finrank K ER < n.succ := by linarith
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) = ⊤
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) = ⊤
have ih_ER : (⨆ (μ : K) (k : ℕ), f'.generalizedEigenspace μ k) = ⊤ :=
  ih (finrank K ER) h_dim_ER f' rfl
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) = ⊤
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) = ⊤
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]
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) = ⊤
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) = ⊤
have hff' :
  ∀ μ k, (f'.generalizedEigenspace μ k).map ER.subtype ≤ f.generalizedEigenspace μ k := by
  intros
  rw [generalizedEigenspace_restrict]
  apply Submodule.map_comap_le
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) = ⊤
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) = ⊤
have hER : ER ≤ ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k := by
  rw [← ih_ER']
  exact iSup₂_mono hff'
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) = ⊤
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) = ⊤
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) μ₀)
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) = ⊤
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) = ⊤
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
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) = ⊤
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) = ⊤
show (⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k) = ⊤
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
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.10506 V
rw [h_dim]
no goals
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
apply Nat.zero_lt_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
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) }
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 }
dsimp only
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) }
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) }
rw [h_dim]
no goals
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) }
apply pos_finrank_generalizedEigenspace_of_hasEigenvalue hμ₀ (Nat.zero_lt_succ n)
no goals
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
apply LinearMap.finrank_range_add_finrank_ker
no goals
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
linarith
no goals
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
simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
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✝
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
intros
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✝
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✝
rw [generalizedEigenspace_restrict]
no goals
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✝
apply Submodule.map_comap_le
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
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
rw [← ih_ER']
no goals
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
exact iSup₂_mono hff'
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
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) = ⊤
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint]
no goals
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
apply sup_le hER hES