-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem generalized_eigenvec_disjoint_range_ker [FiniteDimensional K V] (f : End K V) (μ : K) :
    Disjoint (f.genEigenrange μ (finrank K V))
      (f.genEigenspace μ (finrank K V))

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Tactic:
have h :=
  calc
    Submodule.comap ((f - μ • 1) ^ finrank K V)
      (f.genEigenspace μ (finrank K V)) =
        LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
          (f - algebraMap K (End K V) μ) ^ finrank K V) := by
            rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
    _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
            simp_rw [← pow_add, genEigenspace_nat]; rfl
    _ = f.genEigenspace μ (finrank K V) := by
            rw [genEigenspace_eq_genEigenspace_finrank_of_le]; omega

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Tactic:
rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map,
  Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h, genEigenspace_nat]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Submodule.map ((f - μ • 1) ^ finrank K V) (LinearMap.ker ((f - μ • 1) ^ finrank K V)) ≤ ⊥

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    LinearMap.ker ((f - μ • 1) ^ (finrank K V + finrank K V))

Tactic:
rfl

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) =
    LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V)

Tactic:
rw [genEigenspace_nat, ← LinearMap.ker_comp]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker (((f - μ • 1) ^ finrank K V) ∘ₗ (f - μ • 1) ^ finrank K V) =
    LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Submodule.map ((f - μ • 1) ^ finrank K V) (LinearMap.ker ((f - μ • 1) ^ finrank K V)) ≤ ⊥

Tactic:
apply Submodule.map_comap_le

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(finrank K V + finrank K V) = (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_eq_genEigenspace_finrank_of_le]

Result:
case hk
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ≤ finrank K V + finrank K V

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V) =
    (f.genEigenspace μ) ↑(finrank K V + finrank K V)

Tactic:
simp_rw [← pow_add, genEigenspace_nat]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    LinearMap.ker ((f - μ • 1) ^ (finrank K V + finrank K V))

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker (((f - μ • 1) ^ finrank K V) ∘ₗ (f - μ • 1) ^ finrank K V) =
    LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V)

Tactic:
rfl

Result:
no goals

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

Tactic:
omega

Result:
no goals