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
f : End R M
p : Submodule R M
k : ℕ
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ k) (Submodule.subtype p))
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
f : End R M
p : Submodule R M
k : ℕ
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ ↑(generalizedEigenspace (LinearMap.restrict f hfp) μ) k =
    Submodule.comap (Submodule.subtype p) (↑(generalizedEigenspace f μ) k)
simp only [generalizedEigenspace, OrderHom.coe_fun_mk, ← LinearMap.ker_comp]
case zero
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ Nat.zero) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ Nat.zero) (Submodule.subtype p))

case succ
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
k : ℕ
ih :
  LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ k) (Submodule.subtype p))
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ Nat.succ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ Nat.succ k) (Submodule.subtype p))
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
f : End R M
p : Submodule R M
k : ℕ
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ k) (Submodule.subtype p))
induction' k with k ih
case zero
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker LinearMap.id = LinearMap.ker (LinearMap.comp 1 (Submodule.subtype p))
case zero
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ Nat.zero) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ Nat.zero) (Submodule.subtype p))
rw [pow_zero, pow_zero, LinearMap.one_eq_id]
no goals
case zero
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
⊢ LinearMap.ker LinearMap.id = LinearMap.ker (LinearMap.comp 1 (Submodule.subtype p))
apply (Submodule.ker_subtype _).symm
no goals
case succ
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
f : End R M
p : Submodule R M
μ : R
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
k : ℕ
ih :
  LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ k) (Submodule.subtype p))
⊢ LinearMap.ker ((LinearMap.restrict f hfp - ↑(algebraMap R (End R { x // x ∈ p })) μ) ^ Nat.succ k) =
    LinearMap.ker (LinearMap.comp ((f - ↑(algebraMap R (End R M)) μ) ^ Nat.succ k) (Submodule.subtype p))
erw [pow_succ', pow_succ', LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp,
  LinearMap.comp_assoc]