[GOAL]
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
⊢ eigenspace f 0 = LinearMap.ker f
[PROOFSTEP]
simp [eigenspace]
[GOAL]
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
μ : R
x : M
h : HasEigenvector f μ x
⊢ HasEigenvalue f μ
[PROOFSTEP]
rw [HasEigenvalue, Submodule.ne_bot_iff]
[GOAL]
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
μ : R
x : M
h : HasEigenvector f μ x
⊢ ∃ x, x ∈ eigenspace f μ ∧ x ≠ 0
[PROOFSTEP]
use x
[GOAL]
case h
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
μ : R
x : M
h : HasEigenvector f μ x
⊢ x ∈ eigenspace f μ ∧ x ≠ 0
[PROOFSTEP]
exact h
[GOAL]
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
μ : R
x : M
⊢ x ∈ eigenspace f μ ↔ ↑f x = μ • x
[PROOFSTEP]
rw [eigenspace, LinearMap.mem_ker, LinearMap.sub_apply, algebraMap_end_apply, sub_eq_zero]
[GOAL]
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
μ : R
hμ : HasEigenvalue f μ
⊢ μ ∈ spectrum R f
[PROOFSTEP]
refine' spectrum.mem_iff.mpr fun h_unit => _
[GOAL]
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
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
⊢ False
[PROOFSTEP]
set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
[GOAL]
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
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
⊢ False
[PROOFSTEP]
rcases hμ.exists_hasEigenvector with ⟨v, hv⟩
[GOAL]
case intro
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
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ False
[PROOFSTEP]
refine' hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (_ : μ • v - f v = 0))
[GOAL]
case intro
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
μ : R
hμ : HasEigenvalue f μ
h_unit : IsUnit (↑(algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv (IsUnit.unit h_unit)
v : M
hv : HasEigenvector f μ v
⊢ μ • v - ↑f v = 0
[PROOFSTEP]
rw [hv.apply_eq_smul, sub_self]
[GOAL]
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 : μ ∈ spectrum K f
⊢ HasEigenvalue f μ
[PROOFSTEP]
rwa [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot] at h 
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ eigenspace f (a / b) = eigenspace f (b⁻¹ * a)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm]
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ eigenspace f (b⁻¹ * a) = LinearMap.ker (f - (b⁻¹ * a) • LinearMap.id)
[PROOFSTEP]
rw [eigenspace]
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (f - ↑(algebraMap K (End K V)) (b⁻¹ * a)) = LinearMap.ker (f - (b⁻¹ * a) • LinearMap.id)
[PROOFSTEP]
rfl
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (f - (b⁻¹ * a) • LinearMap.id) = LinearMap.ker (f - b⁻¹ • a • LinearMap.id)
[PROOFSTEP]
rw [smul_smul]
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (f - b⁻¹ • ↑(algebraMap K (End K V)) a) = LinearMap.ker (b • (f - b⁻¹ • ↑(algebraMap K (End K V)) a))
[PROOFSTEP]
rw [LinearMap.ker_smul _ b hb]
[GOAL]
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 K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (b • (f - b⁻¹ • ↑(algebraMap K (End K V)) a)) = LinearMap.ker (b • f - ↑(algebraMap K (End K V)) a)
[PROOFSTEP]
rw [smul_sub, smul_inv_smul₀ hb]
[GOAL]
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 K V
⊢ CompleteLattice.Independent (eigenspace f)
[PROOFSTEP]
classical
  -- Define an operation from `Π₀ μ : K, f.eigenspace μ`, the vector space of finitely-supported
    -- choices of an eigenvector from each eigenspace, to `V`, by sending a collection to its sum.
let S :
  @LinearMap K K _ _ (RingHom.id K) (Π₀ μ : K, f.eigenspace μ) V (@DFinsupp.addCommMonoid K (fun μ => f.eigenspace μ) _)
    _ (@DFinsupp.module K _ (fun μ => f.eigenspace μ) _ _ _) _ :=
  @DFinsupp.lsum K K ℕ _ V _ _ _ _ _ _ _ _ _ fun μ => (f.eigenspace μ).subtype
suffices ∀ l : Π₀ μ, f.eigenspace μ, S l = 0 → l = 0
  by
  rw [CompleteLattice.independent_iff_dfinsupp_lsum_injective]
  change Function.Injective S
  rw [← @LinearMap.ker_eq_bot K K (Π₀ μ, f.eigenspace μ) V _ _ (@DFinsupp.addCommGroup K (fun μ => f.eigenspace μ) _)]
  rw [eq_bot_iff]
  exact this
intro l hl
induction' h_l_support : l.support using Finset.induction with μ₀ l_support' hμ₀ ih generalizing l
· exact DFinsupp.support_eq_empty.1 h_l_support
· let l' := DFinsupp.mapRange.linearMap (fun μ => (μ - μ₀) • @LinearMap.id K (f.eigenspace μ) _ _ _) l
  have h_l_support' : l'.support = l_support' :=
    by
    rw [← Finset.erase_insert hμ₀, ← h_l_support]
    ext a
    have : ¬(a = μ₀ ∨ l a = 0) ↔ ¬a = μ₀ ∧ ¬l a = 0 := not_or
    simp only [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, DFinsupp.mem_support_iff, Finset.mem_erase,
      id.def, LinearMap.id_coe, LinearMap.smul_apply, Ne.def, smul_eq_zero, sub_eq_zero, this]
      -- The entries of `l'` add up to `0`.
  have total_l' : S l' = 0 := by
    let g := f - algebraMap K (End K V) μ₀
    let a : Π₀ _ : K, V := DFinsupp.mapRange.linearMap (fun μ => (f.eigenspace μ).subtype) l
    calc
      S l' = DFinsupp.lsum ℕ (fun μ => (f.eigenspace μ).subtype.comp ((μ - μ₀) • LinearMap.id)) l := ?_
      _ = DFinsupp.lsum ℕ (fun μ => g.comp (f.eigenspace μ).subtype) l := ?_
      _ = DFinsupp.lsum ℕ (fun _ => g) a := ?_
      _ = g (DFinsupp.lsum ℕ (fun _ => (LinearMap.id : V →ₗ[K] V)) a) := ?_
      _ = g (S l) := ?_
      _ = 0 := by rw [hl, g.map_zero]
    · exact DFinsupp.sum_mapRange_index.linearMap
    · congr
      ext μ v
      simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.smul_apply, LinearMap.id_coe, id.def, sub_smul,
        Submodule.subtype_apply, Submodule.coe_sub, Submodule.coe_smul_of_tower, LinearMap.sub_apply,
        mem_eigenspace_iff.1 v.prop, algebraMap_end_apply]
    · rw [DFinsupp.sum_mapRange_index.linearMap]
    ·
      simp only [DFinsupp.sumAddHom_apply, LinearMap.id_coe, LinearMap.map_dfinsupp_sum, id.def,
        LinearMap.toAddMonoidHom_coe, DFinsupp.lsum_apply_apply]
    ·
      simp only [DFinsupp.sum_mapRange_index.linearMap, LinearMap.id_comp]
        -- Therefore, by the induction hypothesis, all entries of `l'` are zero.
  have l'_eq_0 := ih l' total_l' h_l_support'
  have h_smul_eq_0 : ∀ μ, (μ - μ₀) • l μ = 0 := by
    intro μ
    calc
      (μ - μ₀) • l μ = l' μ := by
        simp only [LinearMap.id_coe, id.def, LinearMap.smul_apply, DFinsupp.mapRange_apply,
          DFinsupp.mapRange.linearMap_apply]
      _ = 0 := by rw [l'_eq_0];
        rfl
          -- Thus, the eigenspace-representatives in `l` for all `μ ≠ μ₀` are `0`.
  have h_lμ_eq_0 : ∀ μ : K, μ ≠ μ₀ → l μ = 0 := by
    intro μ hμ
    apply or_iff_not_imp_left.1 (smul_eq_zero.1 (h_smul_eq_0 μ))
    rwa [sub_eq_zero]
      -- So if we sum over all these representatives, we obtain `0`.
  have h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => (l μ : V)) = 0 :=
    by
    rw [← Finset.sum_const_zero]
    apply Finset.sum_congr rfl
    intro μ hμ
    rw [Submodule.coe_eq_zero, h_lμ_eq_0]
    rintro rfl
    exact hμ₀ hμ
  have : l μ₀ = 0 :=
    by
    simp only [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply, LinearMap.toAddMonoidHom_coe, DFinsupp.sum,
      h_l_support, Submodule.subtype_apply, Submodule.coe_eq_zero, Finset.sum_insert hμ₀, h_sum_l_support'_eq_0,
      add_zero] at hl 
    exact hl
  show l = 0
  · ext μ
    by_cases h_cases : μ = μ₀
    · rwa [h_cases, SetLike.coe_eq_coe, DFinsupp.coe_zero, Pi.zero_apply]
    · exact congr_arg _ (h_lμ_eq_0 μ h_cases)
[GOAL]
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 K V
⊢ CompleteLattice.Independent (eigenspace f)
[PROOFSTEP]
let S :
  @LinearMap K K _ _ (RingHom.id K) (Π₀ μ : K, f.eigenspace μ) V (@DFinsupp.addCommMonoid K (fun μ => f.eigenspace μ) _)
    _ (@DFinsupp.module K _ (fun μ => f.eigenspace μ) _ _ _) _ :=
  @DFinsupp.lsum K K ℕ _ V _ _ _ _ _ _ _ _ _ fun μ => (f.eigenspace μ).subtype
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
⊢ CompleteLattice.Independent (eigenspace f)
[PROOFSTEP]
suffices ∀ l : Π₀ μ, f.eigenspace μ, S l = 0 → l = 0
  by
  rw [CompleteLattice.independent_iff_dfinsupp_lsum_injective]
  change Function.Injective S
  rw [← @LinearMap.ker_eq_bot K K (Π₀ μ, f.eigenspace μ) V _ _ (@DFinsupp.addCommGroup K (fun μ => f.eigenspace μ) _)]
  rw [eq_bot_iff]
  exact this
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
this : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
⊢ CompleteLattice.Independent (eigenspace f)
[PROOFSTEP]
rw [CompleteLattice.independent_iff_dfinsupp_lsum_injective]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
this : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
⊢ Function.Injective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (eigenspace f i))
[PROOFSTEP]
change Function.Injective S
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
this : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
⊢ Function.Injective ↑S
[PROOFSTEP]
rw [← @LinearMap.ker_eq_bot K K (Π₀ μ, f.eigenspace μ) V _ _ (@DFinsupp.addCommGroup K (fun μ => f.eigenspace μ) _)]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
this : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
⊢ LinearMap.ker S = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
this : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
⊢ LinearMap.ker S ≤ ⊥
[PROOFSTEP]
exact this
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
⊢ ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → l = 0
[PROOFSTEP]
intro l hl
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
⊢ l = 0
[PROOFSTEP]
induction' h_l_support : l.support using Finset.induction with μ₀ l_support' hμ₀ ih generalizing l
[GOAL]
case empty
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = ∅
⊢ l = 0
[PROOFSTEP]
exact DFinsupp.support_eq_empty.1 h_l_support
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
⊢ l = 0
[PROOFSTEP]
let l' := DFinsupp.mapRange.linearMap (fun μ => (μ - μ₀) • @LinearMap.id K (f.eigenspace μ) _ _ _) l
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
⊢ l = 0
[PROOFSTEP]
have h_l_support' : l'.support = l_support' :=
  by
  rw [← Finset.erase_insert hμ₀, ← h_l_support]
  ext a
  have : ¬(a = μ₀ ∨ l a = 0) ↔ ¬a = μ₀ ∧ ¬l a = 0 := not_or
  simp only [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, DFinsupp.mem_support_iff, Finset.mem_erase,
    id.def, LinearMap.id_coe, LinearMap.smul_apply, Ne.def, smul_eq_zero, sub_eq_zero, this]
    -- The entries of `l'` add up to `0`.
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
⊢ DFinsupp.support l' = l_support'
[PROOFSTEP]
rw [← Finset.erase_insert hμ₀, ← h_l_support]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
⊢ DFinsupp.support l' = Finset.erase (DFinsupp.support l) μ₀
[PROOFSTEP]
ext a
[GOAL]
case a
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
a : K
⊢ a ∈ DFinsupp.support l' ↔ a ∈ Finset.erase (DFinsupp.support l) μ₀
[PROOFSTEP]
have : ¬(a = μ₀ ∨ l a = 0) ↔ ¬a = μ₀ ∧ ¬l a = 0 := not_or
[GOAL]
case a
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
a : K
this : ¬(a = μ₀ ∨ ↑l a = 0) ↔ ¬a = μ₀ ∧ ¬↑l a = 0
⊢ a ∈ DFinsupp.support l' ↔ a ∈ Finset.erase (DFinsupp.support l) μ₀
[PROOFSTEP]
simp only [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, DFinsupp.mem_support_iff, Finset.mem_erase,
  id.def, LinearMap.id_coe, LinearMap.smul_apply, Ne.def, smul_eq_zero, sub_eq_zero, this]
  -- The entries of `l'` add up to `0`.
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
⊢ l = 0
[PROOFSTEP]
have total_l' : S l' = 0 := by
  let g := f - algebraMap K (End K V) μ₀
  let a : Π₀ _ : K, V := DFinsupp.mapRange.linearMap (fun μ => (f.eigenspace μ).subtype) l
  calc
    S l' = DFinsupp.lsum ℕ (fun μ => (f.eigenspace μ).subtype.comp ((μ - μ₀) • LinearMap.id)) l := ?_
    _ = DFinsupp.lsum ℕ (fun μ => g.comp (f.eigenspace μ).subtype) l := ?_
    _ = DFinsupp.lsum ℕ (fun _ => g) a := ?_
    _ = g (DFinsupp.lsum ℕ (fun _ => (LinearMap.id : V →ₗ[K] V)) a) := ?_
    _ = g (S l) := ?_
    _ = 0 := by rw [hl, g.map_zero]
  · exact DFinsupp.sum_mapRange_index.linearMap
  · congr
    ext μ v
    simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.smul_apply, LinearMap.id_coe, id.def, sub_smul,
      Submodule.subtype_apply, Submodule.coe_sub, Submodule.coe_smul_of_tower, LinearMap.sub_apply,
      mem_eigenspace_iff.1 v.prop, algebraMap_end_apply]
  · rw [DFinsupp.sum_mapRange_index.linearMap]
  ·
    simp only [DFinsupp.sumAddHom_apply, LinearMap.id_coe, LinearMap.map_dfinsupp_sum, id.def,
      LinearMap.toAddMonoidHom_coe, DFinsupp.lsum_apply_apply]
  ·
    simp only [DFinsupp.sum_mapRange_index.linearMap, LinearMap.id_comp]
      -- Therefore, by the induction hypothesis, all entries of `l'` are zero.
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
⊢ ↑S l' = 0
[PROOFSTEP]
let g := f - algebraMap K (End K V) μ₀
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
⊢ ↑S l' = 0
[PROOFSTEP]
let a : Π₀ _ : K, V := DFinsupp.mapRange.linearMap (fun μ => (f.eigenspace μ).subtype) l
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑S l' = 0
[PROOFSTEP]
calc
  S l' = DFinsupp.lsum ℕ (fun μ => (f.eigenspace μ).subtype.comp ((μ - μ₀) • LinearMap.id)) l := ?_
  _ = DFinsupp.lsum ℕ (fun μ => g.comp (f.eigenspace μ).subtype) l := ?_
  _ = DFinsupp.lsum ℕ (fun _ => g) a := ?_
  _ = g (DFinsupp.lsum ℕ (fun _ => (LinearMap.id : V →ₗ[K] V)) a) := ?_
  _ = g (S l) := ?_
  _ = 0 := by rw [hl, g.map_zero]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑g (↑S l) = 0
[PROOFSTEP]
rw [hl, g.map_zero]
[GOAL]
case calc_1
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑S l' = ↑(↑(DFinsupp.lsum ℕ) fun μ => LinearMap.comp (Submodule.subtype (eigenspace f μ)) ((μ - μ₀) • LinearMap.id)) l
[PROOFSTEP]
exact DFinsupp.sum_mapRange_index.linearMap
[GOAL]
case calc_2
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑(↑(DFinsupp.lsum ℕ) fun μ => LinearMap.comp (Submodule.subtype (eigenspace f μ)) ((μ - μ₀) • LinearMap.id)) l =
    ↑(↑(DFinsupp.lsum ℕ) fun μ => LinearMap.comp g (Submodule.subtype (eigenspace f μ))) l
[PROOFSTEP]
congr
[GOAL]
case calc_2.e_a.h.e_6.h
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ (fun μ => LinearMap.comp (Submodule.subtype (eigenspace f μ)) ((μ - μ₀) • LinearMap.id)) = fun μ =>
    LinearMap.comp g (Submodule.subtype (eigenspace f μ))
[PROOFSTEP]
ext μ v
[GOAL]
case calc_2.e_a.h.e_6.h.h.h
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
μ : K
v : { x // x ∈ eigenspace f μ }
⊢ ↑(LinearMap.comp (Submodule.subtype (eigenspace f μ)) ((μ - μ₀) • LinearMap.id)) v =
    ↑(LinearMap.comp g (Submodule.subtype (eigenspace f μ))) v
[PROOFSTEP]
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.smul_apply, LinearMap.id_coe, id.def, sub_smul,
  Submodule.subtype_apply, Submodule.coe_sub, Submodule.coe_smul_of_tower, LinearMap.sub_apply,
  mem_eigenspace_iff.1 v.prop, algebraMap_end_apply]
[GOAL]
case calc_3
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑(↑(DFinsupp.lsum ℕ) fun μ => LinearMap.comp g (Submodule.subtype (eigenspace f μ))) l =
    ↑(↑(DFinsupp.lsum ℕ) fun x => g) a
[PROOFSTEP]
rw [DFinsupp.sum_mapRange_index.linearMap]
[GOAL]
case calc_4
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑(↑(DFinsupp.lsum ℕ) fun x => g) a = ↑g (↑(↑(DFinsupp.lsum ℕ) fun x => LinearMap.id) a)
[PROOFSTEP]
simp only [DFinsupp.sumAddHom_apply, LinearMap.id_coe, LinearMap.map_dfinsupp_sum, id.def, LinearMap.toAddMonoidHom_coe,
  DFinsupp.lsum_apply_apply]
[GOAL]
case calc_5
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
g : End K V := f - ↑(algebraMap K (End K V)) μ₀
a : Π₀ (x : K), V := ↑(DFinsupp.mapRange.linearMap fun μ => Submodule.subtype (eigenspace f μ)) l
⊢ ↑g (↑(↑(DFinsupp.lsum ℕ) fun x => LinearMap.id) a) = ↑g (↑S l)
[PROOFSTEP]
simp only [DFinsupp.sum_mapRange_index.linearMap, LinearMap.id_comp]
  -- Therefore, by the induction hypothesis, all entries of `l'` are zero.
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
⊢ l = 0
[PROOFSTEP]
have l'_eq_0 := ih l' total_l' h_l_support'
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
⊢ l = 0
[PROOFSTEP]
have h_smul_eq_0 : ∀ μ, (μ - μ₀) • l μ = 0 := by
  intro μ
  calc
    (μ - μ₀) • l μ = l' μ := by
      simp only [LinearMap.id_coe, id.def, LinearMap.smul_apply, DFinsupp.mapRange_apply,
        DFinsupp.mapRange.linearMap_apply]
    _ = 0 := by rw [l'_eq_0];
      rfl
        -- Thus, the eigenspace-representatives in `l` for all `μ ≠ μ₀` are `0`.
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
⊢ ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
[PROOFSTEP]
intro μ
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
μ : K
⊢ (μ - μ₀) • ↑l μ = 0
[PROOFSTEP]
calc
  (μ - μ₀) • l μ = l' μ := by
    simp only [LinearMap.id_coe, id.def, LinearMap.smul_apply, DFinsupp.mapRange_apply,
      DFinsupp.mapRange.linearMap_apply]
  _ = 0 := by rw [l'_eq_0];
    rfl
      -- Thus, the eigenspace-representatives in `l` for all `μ ≠ μ₀` are `0`.
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
μ : K
⊢ (μ - μ₀) • ↑l μ = ↑l' μ
[PROOFSTEP]
simp only [LinearMap.id_coe, id.def, LinearMap.smul_apply, DFinsupp.mapRange_apply, DFinsupp.mapRange.linearMap_apply]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
μ : K
⊢ ↑l' μ = 0
[PROOFSTEP]
rw [l'_eq_0]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
μ : K
⊢ ↑0 μ = 0
[PROOFSTEP]
rfl
  -- Thus, the eigenspace-representatives in `l` for all `μ ≠ μ₀` are `0`.
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
⊢ l = 0
[PROOFSTEP]
have h_lμ_eq_0 : ∀ μ : K, μ ≠ μ₀ → l μ = 0 := by
  intro μ hμ
  apply or_iff_not_imp_left.1 (smul_eq_zero.1 (h_smul_eq_0 μ))
  rwa [sub_eq_zero]
    -- So if we sum over all these representatives, we obtain `0`.
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
⊢ ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
[PROOFSTEP]
intro μ hμ
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
μ : K
hμ : μ ≠ μ₀
⊢ ↑l μ = 0
[PROOFSTEP]
apply or_iff_not_imp_left.1 (smul_eq_zero.1 (h_smul_eq_0 μ))
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
μ : K
hμ : μ ≠ μ₀
⊢ ¬μ - μ₀ = 0
[PROOFSTEP]
rwa [sub_eq_zero]
  -- So if we sum over all these representatives, we obtain `0`.
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ l = 0
[PROOFSTEP]
have h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => (l μ : V)) = 0 :=
  by
  rw [← Finset.sum_const_zero]
  apply Finset.sum_congr rfl
  intro μ hμ
  rw [Submodule.coe_eq_zero, h_lμ_eq_0]
  rintro rfl
  exact hμ₀ hμ
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
[PROOFSTEP]
rw [← Finset.sum_const_zero]
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ (Finset.sum l_support' fun μ => ↑(↑l μ)) = Finset.sum ?m.347048 fun _x => 0
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ Type ?u.347044
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ Finset ?m.347047
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
⊢ ∀ (x : K), x ∈ l_support' → ↑(↑l x) = 0
[PROOFSTEP]
intro μ hμ
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
μ : K
hμ : μ ∈ l_support'
⊢ ↑(↑l μ) = 0
[PROOFSTEP]
rw [Submodule.coe_eq_zero, h_lμ_eq_0]
[GOAL]
case a
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
μ : K
hμ : μ ∈ l_support'
⊢ μ ≠ μ₀
[PROOFSTEP]
rintro rfl
[GOAL]
case a
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
l_support' : Finset K
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
μ : K
hμ : μ ∈ l_support'
hμ₀ : ¬μ ∈ l_support'
h_l_support : DFinsupp.support l = insert μ l_support'
l' : Π₀ (i : K), { x // x ∈ eigenspace f i } := ↑(DFinsupp.mapRange.linearMap fun μ_1 => (μ_1 - μ) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ_1 : K), (μ_1 - μ) • ↑l μ_1 = 0
h_lμ_eq_0 : ∀ (μ_1 : K), μ_1 ≠ μ → ↑l μ_1 = 0
⊢ False
[PROOFSTEP]
exact hμ₀ hμ
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
⊢ l = 0
[PROOFSTEP]
have : l μ₀ = 0 :=
  by
  simp only [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply, LinearMap.toAddMonoidHom_coe, DFinsupp.sum,
    h_l_support, Submodule.subtype_apply, Submodule.coe_eq_zero, Finset.sum_insert hμ₀, h_sum_l_support'_eq_0,
    add_zero] at hl 
  exact hl
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
⊢ ↑l μ₀ = 0
[PROOFSTEP]
simp only [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply, LinearMap.toAddMonoidHom_coe, DFinsupp.sum, h_l_support,
  Submodule.subtype_apply, Submodule.coe_eq_zero, Finset.sum_insert hμ₀, h_sum_l_support'_eq_0, add_zero] at hl 
[GOAL]
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
hl : ↑l μ₀ = 0
⊢ ↑l μ₀ = 0
[PROOFSTEP]
exact hl
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
this : ↑l μ₀ = 0
⊢ l = 0
[PROOFSTEP]
show l = 0
[GOAL]
case insert
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
this : ↑l μ₀ = 0
⊢ l = 0
[PROOFSTEP]
ext μ
[GOAL]
case insert.h.a
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
this : ↑l μ₀ = 0
μ : K
⊢ ↑(↑l μ) = ↑(↑0 μ)
[PROOFSTEP]
by_cases h_cases : μ = μ₀
[GOAL]
case pos
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
this : ↑l μ₀ = 0
μ : K
h_cases : μ = μ₀
⊢ ↑(↑l μ) = ↑(↑0 μ)
[PROOFSTEP]
rwa [h_cases, SetLike.coe_eq_coe, DFinsupp.coe_zero, Pi.zero_apply]
[GOAL]
case neg
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 K V
S : (Π₀ (μ : K), { x // x ∈ eigenspace f μ }) →ₗ[K] V := ↑(DFinsupp.lsum ℕ) fun μ => Submodule.subtype (eigenspace f μ)
l✝ : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl✝ : ↑S l✝ = 0
x✝ : Finset K
h_l_support✝ : DFinsupp.support l✝ = x✝
μ₀ : K
l_support' : Finset K
hμ₀ : ¬μ₀ ∈ l_support'
ih : ∀ (l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }), ↑S l = 0 → DFinsupp.support l = l_support' → l = 0
l : Π₀ (μ : K), { x // x ∈ eigenspace f μ }
hl : ↑S l = 0
h_l_support : DFinsupp.support l = insert μ₀ l_support'
l' : (fun x => Π₀ (i : K), { x // x ∈ eigenspace f i }) l :=
  ↑(DFinsupp.mapRange.linearMap fun μ => (μ - μ₀) • LinearMap.id) l
h_l_support' : DFinsupp.support l' = l_support'
total_l' : ↑S l' = 0
l'_eq_0 : l' = 0
h_smul_eq_0 : ∀ (μ : K), (μ - μ₀) • ↑l μ = 0
h_lμ_eq_0 : ∀ (μ : K), μ ≠ μ₀ → ↑l μ = 0
h_sum_l_support'_eq_0 : (Finset.sum l_support' fun μ => ↑(↑l μ)) = 0
this : ↑l μ₀ = 0
μ : K
h_cases : ¬μ = μ₀
⊢ ↑(↑l μ) = ↑(↑0 μ)
[PROOFSTEP]
exact congr_arg _ (h_lμ_eq_0 μ h_cases)
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
⊢ (fun k => LinearMap.ker ((f - ↑(algebraMap R (End R M)) μ) ^ k)) k ≤
    (fun k => LinearMap.ker ((f - ↑(algebraMap R (End R M)) μ) ^ k)) m
[PROOFSTEP]
simp only [← pow_sub_mul_pow _ hm]
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
⊢ LinearMap.ker ((f - ↑(algebraMap R (End R M)) μ) ^ k) ≤
    LinearMap.ker ((f - ↑(algebraMap R (End R M)) μ) ^ (m - k) * (f - ↑(algebraMap R (End R M)) μ) ^ k)
[PROOFSTEP]
exact LinearMap.ker_le_ker_comp ((f - algebraMap R (End R M) μ) ^ k) ((f - algebraMap R (End R M) μ) ^ (m - k))
[GOAL]
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
k : ℕ
⊢ ↑(generalizedEigenspace f 0) k = LinearMap.ker (f ^ k)
[PROOFSTEP]
simp [Module.End.generalizedEigenspace]
[GOAL]
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
μ : R
k : ℕ
h : HasGeneralizedEigenvalue f μ k
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
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
μ : R
h : HasGeneralizedEigenvalue f μ 0
⊢ False
[PROOFSTEP]
exact h LinearMap.ker_id
[GOAL]
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
μ : R
m : M
⊢ m ∈ maximalGeneralizedEigenspace f μ ↔ ∃ k, ↑((f - μ • 1) ^ k) m = 0
[PROOFSTEP]
simp only [maximalGeneralizedEigenspace, ← mem_generalizedEigenspace, Submodule.mem_iSup_of_chain]
[GOAL]
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
h : IsNoetherian R M
f : End R M
μ : R
⊢ maximalGeneralizedEigenspace f μ = ↑(generalizedEigenspace f μ) (maximalGeneralizedEigenspaceIndex f μ)
[PROOFSTEP]
rw [isNoetherian_iff_wellFounded] at h 
[GOAL]
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
h : WellFounded fun x x_1 => x > x_1
f : End R M
μ : R
⊢ maximalGeneralizedEigenspace f μ = ↑(generalizedEigenspace f μ) (maximalGeneralizedEigenspaceIndex f μ)
[PROOFSTEP]
exact (WellFounded.iSup_eq_monotonicSequenceLimit h (f.generalizedEigenspace μ) : _)
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
hk : HasGeneralizedEigenvalue f μ k
⊢ HasGeneralizedEigenvalue f μ m
[PROOFSTEP]
unfold HasGeneralizedEigenvalue at *
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) k ≠ ⊥
⊢ ↑(generalizedEigenspace f μ) m ≠ ⊥
[PROOFSTEP]
contrapose! hk
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(generalizedEigenspace f μ) k = ⊥
[PROOFSTEP]
rw [← le_bot_iff, ← hk]
[GOAL]
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
μ : R
k m : ℕ
hm : k ≤ m
hk : ↑(generalizedEigenspace f μ) m = ⊥
⊢ ↑(generalizedEigenspace f μ) k ≤ ↑(generalizedEigenspace f μ) m
[PROOFSTEP]
exact (f.generalizedEigenspace μ).monotone hm
[GOAL]
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
μ : R
k : ℕ
hk : 0 < k
hμ : HasEigenvalue f μ
⊢ HasGeneralizedEigenvalue f μ k
[PROOFSTEP]
apply hasGeneralizedEigenvalue_of_hasGeneralizedEigenvalue_of_le hk
[GOAL]
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
μ : R
k : ℕ
hk : 0 < k
hμ : HasEigenvalue f μ
⊢ HasGeneralizedEigenvalue f μ (Nat.succ 0)
[PROOFSTEP]
rw [HasGeneralizedEigenvalue, generalizedEigenspace, OrderHom.coe_mk, pow_one]
[GOAL]
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
μ : R
k : ℕ
hk : 0 < k
hμ : HasEigenvalue f μ
⊢ LinearMap.ker (f - ↑(algebraMap R (End R M)) μ) ≠ ⊥
[PROOFSTEP]
exact hμ
[GOAL]
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
μ : R
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
⊢ HasEigenvalue f μ
[PROOFSTEP]
intro contra
[GOAL]
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
μ : R
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace f μ = ⊥
⊢ False
[PROOFSTEP]
apply hμ
[GOAL]
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
μ : R
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : eigenspace f μ = ⊥
⊢ ↑(generalizedEigenspace f μ) k = ⊥
[PROOFSTEP]
erw [LinearMap.ker_eq_bot] at contra ⊢
[GOAL]
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
μ : R
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective ↑((f - ↑(algebraMap R (End R M)) μ) ^ k)
[PROOFSTEP]
rw [LinearMap.coe_pow]
[GOAL]
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
μ : R
k : ℕ
hμ : HasGeneralizedEigenvalue f μ k
contra : Function.Injective ↑(f - ↑(algebraMap R (End R M)) μ)
⊢ Function.Injective (↑(f - ↑(algebraMap R (End R M)) μ))^[k]
[PROOFSTEP]
exact Function.Injective.iterate contra k
[GOAL]
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)
[PROOFSTEP]
simp only [generalizedEigenspace, OrderHom.coe_mk, ← LinearMap.ker_comp]
[GOAL]
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))
[PROOFSTEP]
induction' k with k ih
[GOAL]
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))
[PROOFSTEP]
rw [pow_zero, pow_zero, LinearMap.one_eq_id]
[GOAL]
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))
[PROOFSTEP]
apply (Submodule.ker_subtype _).symm
[GOAL]
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))
[PROOFSTEP]
erw [pow_succ', pow_succ', LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp, LinearMap.comp_assoc]
[GOAL]
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
⊢ Submodule.map (Submodule.subtype p) (eigenspace (LinearMap.restrict f hfp) μ) ≤ eigenspace f μ
[PROOFSTEP]
rintro a ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ ↑(Submodule.subtype p) x ∈ eigenspace f μ
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢
[GOAL]
case intro.intro
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
x : { x // x ∈ p }
hx : { val := ↑f ↑x, property := (_ : ↑f ↑x ∈ p) } = μ • x
⊢ ↑f (↑(Submodule.subtype p) x) = μ • ↑(Submodule.subtype p) x
[PROOFSTEP]
exact congr_arg Subtype.val hx
[GOAL]
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))
[PROOFSTEP]
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_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
[GOAL]
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)
[PROOFSTEP]
rw [generalizedEigenspace, OrderHom.coe_mk, ← LinearMap.ker_comp]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
rw [← pow_add]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
rw [generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le]
[GOAL]
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
[PROOFSTEP]
linarith
[GOAL]
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))
[PROOFSTEP]
rw [disjoint_iff_inf_le, generalizedEigenrange, LinearMap.range_eq_map, Submodule.map_inf_eq_map_inf_comap, top_inf_eq,
  h]
[GOAL]
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)) ≤ ⊥
[PROOFSTEP]
apply Submodule.map_comap_le
[GOAL]
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
[PROOFSTEP]
intro x hx
[GOAL]
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
hfp : ∀ (x : M), x ∈ p → ↑f x ∈ p
μ : R
hμp : Disjoint (eigenspace f μ) p
x : { x // x ∈ p }
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ x ∈ ⊥
[PROOFSTEP]
simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩
[GOAL]
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 : ℕ
μ : K
hx : HasEigenvalue f μ
hk : 0 < k
⊢ 0 = finrank K { x // x ∈ ⊥ }
[PROOFSTEP]
rw [finrank_bot]
[GOAL]
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 K V
μ : K
n : ℕ
⊢ Submodule.map f (generalizedEigenrange f μ n) = LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n)
[PROOFSTEP]
rw [generalizedEigenrange]
[GOAL]
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 K V
μ : K
n : ℕ
⊢ Submodule.map f (LinearMap.range ((f - ↑(algebraMap K (End K V)) μ) ^ n)) =
    LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n)
[PROOFSTEP]
exact (LinearMap.range_comp _ _).symm
[GOAL]
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 K V
μ : K
n : ℕ
⊢ LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n) =
    LinearMap.range ((f - ↑(algebraMap K (End K V)) μ) ^ n * f)
[PROOFSTEP]
rw [Algebra.mul_sub_algebraMap_pow_commutes]
