K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V)
⊢ Disjoint (generalizedEigenrange f μ (finrank K V)) (↑(generalizedEigenspace f μ) (finrank K V))
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Disjoint (generalizedEigenrange f μ (finrank K V)) (↑(generalizedEigenspace f μ) (finrank K V))
have h :=
  calc
    Submodule.comap ((f - algebraMap _ _ μ) ^ finrank K V)
      (f.generalizedEigenspace μ (finrank K V)) =
        LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
          (f - algebraMap K (End K V) μ) ^ finrank K V) := by
            rw [generalizedEigenspace, OrderHom.coe_fun_mk, ← LinearMap.ker_comp]; rfl
    _ = f.generalizedEigenspace μ (finrank K V + finrank K V) := by rw [← pow_add]; rfl
    _ = f.generalizedEigenspace μ (finrank K V) := by
      rw [generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le]; linarith
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V)
⊢ Submodule.map ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) ≤ ⊥
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V)
⊢ Disjoint (generalizedEigenrange f μ (finrank K V)) (↑(generalizedEigenspace f μ) (finrank K V))
rw [disjoint_iff_inf_le, generalizedEigenrange, LinearMap.range_eq_map,
  Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h]
no goals
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V)
⊢ Submodule.map ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) ≤ ⊥
apply Submodule.map_comap_le
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker
      (LinearMap.comp ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)
        ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)) =
    LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V * (f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Submodule.comap ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) (↑(generalizedEigenspace f μ) (finrank K V)) =
    LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V * (f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)
rw [generalizedEigenspace, OrderHom.coe_fun_mk, ← LinearMap.ker_comp]
no goals
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker
      (LinearMap.comp ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)
        ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)) =
    LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V * (f - ↑(algebraMap K (End K V)) μ) ^ finrank K V)
rfl
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V + finrank K V)
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ finrank K V * (f - ↑(algebraMap K (End K V)) μ) ^ finrank K V) =
    ↑(generalizedEigenspace f μ) (finrank K V + finrank K V)
rw [← pow_add]
no goals
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - ↑(algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ↑(generalizedEigenspace f μ) (finrank K V + finrank K V)
rfl
case hk
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ≤ finrank K V + finrank K V
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ ↑(generalizedEigenspace f μ) (finrank K V + finrank K V) = ↑(generalizedEigenspace f μ) (finrank K V)
rw [generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le]
no goals
case hk
K R : Type v
V M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ≤ finrank K V + finrank K V
linarith