@Aristotle-Harmonic 's proof on Lean 4.20 that a linear map is diagonalizable iff the minpoly is a product of distinct linear factors.

diagonalizable_iff_minpoly.lean

/--
An common eigenbasis (a.k.a. simultaneous diagonalization) of a family of linear maps
$T_i : V to V$ is a basis of $V$ consisting of common eigenvectors of $T_i$.

Simultaneous diagonalizability is the existence of a common eigenbasis, spelled as
`∃ ι : Type u, Nonempty (CommonEigenbasis ι f)` with the naming convention
`exists_commonEigenbasis`.
-/
structure LinearMap.CommonEigenbasis {α S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] (ι : Type*) (f : α → Module.End S M) extends Basis ι S M where
  /-- The eigenvalues of the eigenbasis. -/
  μ : α → ι → S
  /--
  The eigenvector property. The definition matches `Module.End.HasEigenvector.apply_eq_smul`,
  but we don't use `Module.End.HasEigenvector`, as it's slightly more convenient to admit the
  degenerate bases over the trivial ring; for `Nontrivial R`, we can still get
  `CommonEigenbasis.ofHasEigenVector` and `CommonEigenbasis.hasEigenVector_μ`.
  -/
  apply_eq_smul (a : α) (i : ι) : f a (toBasis i) = μ a i • toBasis i

/--
An eigenbasis (a.k.a. diagonalization) of a linear map $T : V to V$ is a basis of $V$
consisting of eigenvectors of $T$.

Diagonalizability is the existence of an eigenbasis, spelled as
`∃ ι : Type u, Nonempty (f.Eigenbasis ι)` with the naming convention `exists_eigenbasis`.
-/
def LinearMap.Eigenbasis {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] (ι : Type*) (f : Module.End S M) := CommonEigenbasis ι fun _ : Unit ↦ f

def LinearMap.Eigenbasis.μ {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] {ι : Type*} {f : Module.End S M} (self : f.Eigenbasis ι) : ι → S :=
  CommonEigenbasis.μ self ()

lemma aeval_prod_X_sub_C_eigenvalues_eq_zero.{uG} {ι R : Type*} {G : Type uG} [CommRing R] [IsDomain R] [AddCommGroup G] [Module R G] [Module.Free R G] [Module.Finite R G] {f : Module.End R G} (B : f.Eigenbasis ι) :
    haveI : Finite ι := Module.Finite.finite_basis B.toBasis
    Polynomial.aeval f (∏ a ∈ (Set.range B.μ).toFinite.toFinset, (Polynomial.X - Polynomial.C a)) = 0 := by
  -- Since $B$ is an eigenbasis, for each $i$, we have $f(v_i) = \mu_i v_i$.
  have h_eigen : ∀ i, f (B.toBasis i) = B.μ i • B.toBasis i := by
    exact fun i => B.apply_eq_smul _ i
  generalize_proofs at *;
  -- Apply the polynomial to each basis vector using the fact that $f(v_i) = \mu_i v_i$.
  have h_apply : ∀ i, (Polynomial.aeval f (∏ a in (Set.Finite.toFinset ‹Set.Finite (Set.range B.μ)›), (Polynomial.X - Polynomial.C a))) (B.toBasis i) = 0 := by
    aesop;
    -- Since $B$ is an eigenbasis, for each $i$, we have $f(v_i) = \mu_i v_i$. Therefore, $(f - C(\mu_i))(v_i) = 0$.
    have h_factor : (f - (algebraMap R (Module.End R G)) (B.μ i)) (B.toBasis i) = 0 := by
      simp ( config := { decide := Bool.true } ) [ h_eigen i ];
    rw [ Finset.prod_eq_prod_diff_singleton_mul <| pf_2.mem_toFinset.mpr <| Set.mem_range_self i ] ; simp ( config := { decide := Bool.true } ) [ h_factor ] ;
  refine' Basis.ext ( B.toBasis ) _;
  -- Apply the hypothesis `h_apply` to each `i`.
  intro i
  apply h_apply


lemma minpoly_eq_prod_X_sub_C_eigenvalues.{uG} {ι R : Type*} {G : Type uG} [CommRing R] [IsDomain R] [AddCommGroup G] [Module R G] [Module.Free R G] [Module.Finite R G] {f : Module.End R G} (B : f.Eigenbasis ι) :
    haveI : Finite ι := Module.Finite.finite_basis B.toBasis
    minpoly R f = (∏ a ∈ (Set.range B.μ).toFinite.toFinset, (Polynomial.X - Polynomial.C a)) := by
  symm
  generalize_proofs at *;
  apply minpoly.unique' R f;
  · exact Polynomial.monic_prod_of_monic _ _ fun x hx => Polynomial.monic_X_sub_C x;
  · convert aeval_prod_X_sub_C_eigenvalues_eq_zero B using 1;
  · rw [ Polynomial.degree_prod, Finset.sum_congr rfl fun _ _ => Polynomial.degree_X_sub_C _ ] ; aesop;
    refine' Classical.or_iff_not_imp_left.2 fun hq => _;
    -- Since $q$ is a polynomial of degree less than the cardinality of the set of eigenvalues, there exists an eigenvalue $c$ such that $q(c) \neq 0$.
    obtain ⟨c, hc⟩ : ∃ c ∈ Set.range B.μ, q.eval c ≠ 0 := by
      contrapose! a;
      have h_card_roots : q.roots.toFinset.card ≥ pf.toFinset.card := by
        exact Finset.card_le_card fun x hx => by aesop;
      rw [ Polynomial.degree_eq_natDegree hq ] ; exact_mod_cast h_card_roots.trans ( Multiset.toFinset_card_le _ ) |> le_trans <| Polynomial.card_roots' _;
    -- Let $v$ be the eigenvector corresponding to $c$.
    obtain ⟨v, hv⟩ : ∃ v : G, v ≠ 0 ∧ f v = c • v := by
      rcases hc.1 with ⟨ i, rfl ⟩ ; exact ⟨ B.toBasis i, B.toBasis.ne_zero i, B.apply_eq_smul _ _ ⟩ ;
    -- Apply $q(f)$ to the eigenvector $v$.
    have h_apply_q : (Polynomial.aeval f q) v = q.eval c • v := by
      simp ( config := { decide := Bool.true } ) [ Polynomial.aeval_eq_sum_range, Polynomial.eval_eq_sum_range, hv ];
      -- By definition of exponentiation, we know that $(f^x) v = c^x • v$ for any $x$.
      have h_exp : ∀ x : ℕ, (f ^ x) v = c ^ x • v := by
        intro x; induction x <;> simp_all ( config := { decide := Bool.true } ) [ pow_succ', MulAction.mul_smul ] ;
        rw [ SMulCommClass.smul_comm ];
      simp ( config := { decide := Bool.true } ) only [ h_exp, Finset.sum_smul, MulAction.mul_smul ];
    exact fun h => hv.1 ( by simpa [ h, hc.2 ] using h_apply_q.symm )


def projection_polynomial_numerator (R : Type*) [Field R] (s : Finset R) (a : R) : Polynomial R :=
  ∏ i in s.erase a, (Polynomial.X - Polynomial.C i)

def projection_polynomial_denominator (R : Type*) [Field R] (s : Finset R) (a : R) : R :=
  (projection_polynomial_numerator R s a).eval a

def projection_polynomial (R : Type*) [Field R] (s : Finset R) (a : R) : Polynomial R :=
  projection_polynomial_numerator R s a * Polynomial.C (1 / projection_polynomial_denominator R s a)

lemma eval_projection_polynomial {R : Type*} [Field R] {s : Finset R} (h_distinct : (s : Set R).Pairwise (fun a b => a ≠ b)) (a b : R) (ha : a ∈ s) (hb : b ∈ s) :
  (projection_polynomial R s a).eval b = if a = b then 1 else 0 := by
    aesop;
    · unfold projection_polynomial;
      simp ( config := { decide := Bool.true } ) [ Finset.prod_eq_prod_diff_singleton_mul hb, projection_polynomial_denominator, projection_polynomial_numerator ];
      simp ( config := { decide := Bool.true } ) [ Polynomial.eval_prod, Finset.prod_eq_zero_iff, sub_eq_zero ];
    · -- Since $b \in s$ and $a \neq b$, one of the factors in the numerator $\prod_{i \in s \setminus \{a\}} (b - i)$ will be $(b - a)$, which is zero.
      have h_num_zero : Polynomial.eval b (projection_polynomial_numerator R s a) = 0 := by
        have h_num_zero : b ∈ s.erase a := by
          aesop;
        exact Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero ( Finset.dvd_prod_of_mem _ h_num_zero ) ( by simp ( config := { decide := Bool.true } ) );
      simp_all ( config := { decide := Bool.true } ) [ projection_polynomial ]


lemma sum_projection_polynomials_eq_one {R : Type*} [Field R] {s : Finset R} (h_distinct : (s : Set R).Pairwise (fun a b => a ≠ b)) (hs : s.Nonempty) :
  ∑ a in s, projection_polynomial R s a = 1 := by
    refine' Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq _ _ _ <;> aesop;
    · refine' lt_of_le_of_lt ( Polynomial.degree_sub_le _ _ ) _ ; aesop;
      erw [ Polynomial.degree_lt_iff_coeff_zero ];
      aesop;
      refine Finset.sum_eq_zero fun x hx => ?_;
      -- Since $m \geq s.card$, the degree of the numerator is less than $m$, so the coefficient of $m$ in the numerator is zero.
      have h_num_deg : Polynomial.degree (projection_polynomial_numerator R s x) < m := by
        simp ( config := { decide := Bool.true } ) [ projection_polynomial_numerator, Polynomial.degree_prod ];
        exact lt_of_lt_of_le ( Finset.card_lt_card ( Finset.erase_ssubset hx ) ) a;
      -- Since the degree of the numerator is less than m, the coefficient of m in the numerator is zero.
      have h_num_coeff : Polynomial.coeff (projection_polynomial_numerator R s x) m = 0 := by
        exact Polynomial.coeff_eq_zero_of_degree_lt h_num_deg;
      simp_all ( config := { decide := Bool.true } ) [ projection_polynomial ];
    · -- Since $x \in s$, for any $a \in s$ with $a \neq x$, the projection polynomial $projection\_polynomial R s a$ evaluated at $x$ is zero.
      have h_zero : ∀ a ∈ s, a ≠ x → (projection_polynomial R s a).eval x = 0 := by
        -- Since $x \in s$ and $a \neq x$, $x$ is in the set $s.erase a$, so one of the factors in the numerator is $(x - x) = 0$.
        intros a ha hax
        have hx_erase : x ∈ s.erase a := by
          aesop;
        simp ( config := { decide := Bool.true } ) [ projection_polynomial, Polynomial.eval_prod, Finset.prod_eq_zero hx_erase ];
        exact Or.inl ( by rw [ projection_polynomial_numerator ] ; exact Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero ( Finset.dvd_prod_of_mem _ hx_erase ) ( by simp ( config := { decide := Bool.true } ) ) );
      -- Since $x \in s$, the projection polynomial for $x$ evaluated at $x$ is 1.
      have h_x : (projection_polynomial R s x).eval x = 1 := by
        rw [ projection_polynomial ];
        unfold projection_polynomial_numerator projection_polynomial_denominator; aesop;
        unfold projection_polynomial_numerator; simp ( config := { decide := Bool.true } ) [ Polynomial.eval_prod, Finset.prod_eq_zero_iff, sub_eq_zero ] ;
      rw [ Polynomial.eval_finset_sum, Finset.sum_eq_single x ] <;> aesop


lemma module_primary_decomposition {R M : Type*} [Field R] [AddCommGroup M] [Module R M] [FiniteDimensional R M] {f : Module.End R M} {s : Finset R} (h_min_poly : minpoly R f = ∏ a in s, (Polynomial.X - Polynomial.C a)) (h_distinct : (s : Set R).Pairwise (fun a b => a ≠ b)) :
  CompleteLattice.Independent (fun a : s => LinearMap.ker (f - (↑a : R) • 1)) ∧
  (⨆ a : s, LinearMap.ker (f - (↑a : R) • 1)) = ⊤ := by
    -- To prove the direct sum, we show that the sum of the kernels is direct and that it spans M.
    have h_direct_sum : ⨆ a : { x // x ∈ s }, LinearMap.ker (f - (a : R) • 1) = ⊤ := by
      -- Since the minimal polynomial of $f$ is the product of distinct linear factors, the vector space $M$ is the direct sum of the eigenspaces corresponding to each eigenvalue in $s$.
      have h_decomp : ∀ m : M, ∃ (v : s → M), (∀ a : s, (f - (a : R) • 1) (v a) = 0) ∧ m = ∑ a : s, v a := by
        -- Let's choose any $m \in M$.
        intro m
        -- Since $\prod_{a \in s} (X - a) = 0$, we have $m = \sum_{a \in s} \pi_a(m)$ where $\pi_a$ are projection operators.
        have h_decomp_step : m = ∑ a in s, (Polynomial.aeval f (projection_polynomial R s a)) m := by
          -- By definition of projection polynomials, we know that $\sum_{a \in s} \pi_a = 1$.
          have h_sum_proj : ∑ a in s, (Polynomial.aeval f (projection_polynomial R s a)) = 1 := by
            by_cases hs : s.Nonempty <;> aesop;
            · -- By definition of projection polynomials, we know that $\sum_{a \in s} \pi_a = 1$ as a polynomial.
              have h_sum_proj_poly : ∑ a in s, projection_polynomial R s a = 1 := by
                exact?;
              simpa using congr_arg ( Polynomial.aeval f ) h_sum_proj_poly;
            · have := minpoly.aeval R f; aesop;
          simpa using congr_arg ( fun g : Module.End R M => g m ) h_sum_proj.symm;
        -- Each term in the sum $\sum_{a \in s} \pi_a(m)$ is in the kernel of $f - aI$.
        have h_kernel : ∀ a ∈ s, (f - (a : R) • 1) ((Polynomial.aeval f (projection_polynomial R s a)) m) = 0 := by
          intro a ha
          have h_eval : (f - (a : R) • 1) ∘ₗ (Polynomial.aeval f (projection_polynomial R s a)) = 0 := by
            -- Since the projection polynomial is constructed such that when multiplied by (X - a), it becomes divisible by the minimal polynomial, we can conclude that (f - a • 1) composed with the projection polynomial is zero.
            have h_div : (Polynomial.X - Polynomial.C a) * projection_polynomial R s a = (∏ b in s, (Polynomial.X - Polynomial.C b)) * Polynomial.C (1 / projection_polynomial_denominator R s a) := by
              simp ( config := { decide := Bool.true } ) [ projection_polynomial, Finset.prod_erase_mul _ _ ha ];
              rw [ ← mul_assoc, ← Finset.mul_prod_erase _ _ ha ];
              rfl;
            have h_eval_zero : Polynomial.aeval f (∏ b in s, (Polynomial.X - Polynomial.C b)) = 0 := by
              rw [ ← h_min_poly, minpoly.aeval ];
            replace h_div := congr_arg ( Polynomial.aeval f ) h_div ; simp ( config := { decide := Bool.true } ) [ h_eval_zero ] at h_div ⊢ ; aesop ( simp_config := { singlePass := Bool.true } ) ;
          exact LinearMap.congr_fun h_eval m;
        refine' ⟨ fun a => ( Polynomial.aeval f ( projection_polynomial R s a ) ) m, _, _ ⟩ <;> simp ( config := { decide := Bool.true } ) [ h_kernel ] at h_decomp_step ⊢;
        convert h_decomp_step using 1;
        conv_rhs => rw [ ← Finset.sum_attach ] ;
      refine' eq_top_iff.mpr fun m hm => _;
      rcases h_decomp m with ⟨ v, hv, rfl ⟩;
      exact Submodule.sum_mem _ fun a _ => Submodule.mem_iSup_of_mem a <| by simpa using hv a;
    refine' ⟨ _, h_direct_sum ⟩;
    -- To prove the independence, assume that $\sum_{a \in s} v_a = 0$ where $v_a \in \ker(f - a \cdot \text{id})$.
    have h_indep : ∀ (v : s → M), (∀ a : s, (f - (a : R) • 1) (v a) = 0) → (∑ a : s, v a = 0) → ∀ a : s, v a = 0 := by
      intro v hv hv' a
      have h_apply_poly : ∀ p : Polynomial R, p.eval₂ (algebraMap R (Module.End R M)) f (v a) = p.eval (a : R) • v a := by
        -- By definition of polynomial evaluation, we can expand $p(f)(v_a)$ using the linearity of $f$.
        have h_poly_eval : ∀ p : Polynomial R, (Polynomial.eval₂ (algebraMap R (Module.End R M)) f p) (v a) = Polynomial.eval (a : R) p • v a := by
          intro p
          have h_ind : ∀ n : ℕ, (f ^ n) (v a) = (a : R) ^ n • v a := by
            intro n; induction n <;> simp_all ( config := { decide := Bool.true } ) [ pow_succ', smul_smul ] ;
            simp_all ( config := { decide := Bool.true } ) [ sub_eq_zero, mul_comm, MulAction.mul_smul ];
            rw [ SMulCommClass.smul_comm ]
          simp ( config := { decide := Bool.true } ) [ Polynomial.eval₂_eq_sum_range, Polynomial.eval_eq_sum_range, h_ind ];
          simp ( config := { decide := Bool.true } ) [ mul_comm, Finset.sum_smul, smul_smul ];
        exact h_poly_eval;
      -- Let $p_a(x) = \prod_{b \in s, b \neq a} (x - b)$.
      set p_a : Polynomial R := ∏ b in s.erase a, (Polynomial.X - Polynomial.C b);
      -- Since $p_a(f)(v_b) = 0$ for all $b \neq a$, we have $p_a(f)(\sum_{b \in s} v_b) = p_a(f)(v_a)$.
      have h_apply_pa_simplified : p_a.eval₂ (algebraMap R (Module.End R M)) f (∑ b : s, v b) = p_a.eval₂ (algebraMap R (Module.End R M)) f (v a) := by
        have h_apply_pa_simplified : ∀ b : s, b ≠ a → p_a.eval₂ (algebraMap R (Module.End R M)) f (v b) = 0 := by
          intro b hb_ne_a
          have h_apply_pa_b : (Polynomial.eval₂ (algebraMap R (Module.End R M)) f (Polynomial.X - Polynomial.C (b : R))) (v b) = 0 := by
            simpa [ sub_eq_zero ] using hv b;
          simp +zetaDelta at *;
          rw [ Finset.prod_eq_prod_diff_singleton_mul <| Finset.mem_erase_of_ne_of_mem ( by simpa [ Subtype.ext_iff ] using hb_ne_a ) b.2 ] ; simp ( config := { decide := Bool.true } ) [ hv ];
        rw [ map_sum, Finset.sum_eq_single a ] <;> aesop;
      rw [ eq_comm ] at h_apply_pa_simplified ; aesop;
      simp_all ( config := { decide := Bool.true } ) [ Polynomial.eval_prod, Finset.prod_eq_zero_iff, sub_eq_iff_eq_add ];
    refine' fun a => _;
    simp ( config := { decide := Bool.true } ) [ disjoint_iff_inf_le ];
    rw [ Submodule.eq_bot_iff ];
    intro x hx
    obtain ⟨hx_ker, hx_sum⟩ := hx;
    -- By definition of supremum, there exist elements $y_j \in \ker(f - j \cdot \text{id})$ for $j \neq a$ such that $x = \sum_{j \neq a} y_j$.
    obtain ⟨y, hy⟩ : ∃ y : { x // x ∈ s } → M, (∀ j : { x // x ∈ s }, j ≠ a → y j ∈ LinearMap.ker (f - (j : R) • 1)) ∧ x = ∑ j in Finset.univ.erase a, y j := by
      have h_decomp : x ∈ Submodule.span R (⋃ j ∈ Finset.univ.erase a, LinearMap.ker (f - (j : R) • 1)) := by
        simp ( config := { decide := Bool.true } ) [ Submodule.span_iUnion ];
        exact?;
      refine' Submodule.span_induction _ _ _ _ h_decomp;
      · simp +zetaDelta at *;
        intro x b hb hb' hx; use fun j => if j = ⟨ b, hb ⟩ then x else 0; aesop;
      · exact ⟨ fun _ => 0, fun _ _ => by simp ( config := { decide := Bool.true } ), by simp ( config := { decide := Bool.true } ) ⟩;
      · rintro x y hx hy ⟨ u, hu, rfl ⟩ ⟨ v, hv, rfl ⟩ ; exact ⟨ u + v, fun j hj => by simpa using hu j hj |> AddSubmonoid.add_mem _ <| hv j hj, by simp ( config := { decide := Bool.true } ) [ Finset.sum_add_distrib ] ⟩ ;
      · rintro r x hx ⟨ y, hy, rfl ⟩;
        refine' ⟨ fun j => r • y j, fun j hj => _, _ ⟩ <;> simp ( config := { decide := Bool.true } ) [ Finset.smul_sum, hy ];
        · exact Or.inr ( LinearMap.mem_ker.mp ( hy j hj ) );
        · simp ( config := { decide := Bool.true } ) [ Finset.smul_sum, smul_sub ];
    specialize h_indep ( fun j => if j = a then -x else y j ) ; simp_all ( config := { decide := Bool.true } ) [ Finset.sum_ite, Finset.filter_ne' ];
    contrapose! h_indep;
    refine' ⟨ _, _, _ ⟩;
    · intro b hb; split_ifs with h <;> simp_all ( config := { decide := Bool.true } ) [ sub_eq_iff_eq_add ] ;
      rw [ ← smul_neg, neg_sub ];
    · simp ( config := { decide := Bool.true } ) [ Finset.filter_eq', Finset.card_singleton ];
    · refine' ⟨ a, a.2, _ ⟩ ; simp ( config := { decide := Bool.true } ) [ h_indep ];
      exact fun h => h_indep <| by rw [ sub_eq_zero ] at h; aesop;


lemma problem1.{uG} {R : Type*} {G : Type uG} [Field R] [AddCommGroup G] [Module R G] [Module.Finite R G] {f : Module.End R G}
    (h : ∃ s : Finset R, minpoly R f = (∏ a ∈ s, (Polynomial.X - Polynomial.C a))) :
    ∃ (ι : Type uG), (Nonempty (f.Eigenbasis ι)) := by
  -- Since the minimal polynomial splits, the eigenspaces corresponding to each eigenvalue span the entire space G. Therefore, we can take the union of these eigenspaces to form a basis.
  obtain ⟨s, hs⟩ := h;
  have h_eigenspaces : ⨆ a ∈ s, LinearMap.ker (f - (a : R) • 1) = ⊤ := by
    have h_decomp : CompleteLattice.Independent (fun a : s => LinearMap.ker (f - (↑a : R) • 1)) ∧ (⨆ a : s, LinearMap.ker (f - (↑a : R) • 1)) = ⊤ := by
      -- Since the minimal polynomial of $f$ is a product of distinct linear factors, the roots of the minimal polynomial are distinct.
      have h_distinct : (s : Set R).Pairwise (fun a b => a ≠ b) := by
        exact fun x hx y hy hxy => hxy;
      exact?;
    convert h_decomp.2 using 1;
    rw [ iSup_subtype ];
  -- Since the eigenspaces corresponding to each eigenvalue span the entire space G, we can take the union of these eigenspaces to form a basis.
  obtain ⟨T, hT⟩ : ∃ T : Set G, (Submodule.span R T = ⊤) ∧ (∀ v ∈ T, ∃ a ∈ s, f v = a • v) := by
    -- For each $a \in s$, let $T_a$ be a basis of $\ker(f - aI)$.
    have h_basis_eigenspaces : ∀ a ∈ s, ∃ T_a : Set G, (Submodule.span R T_a = LinearMap.ker (f - a • 1)) ∧ (∀ v ∈ T_a, f v = a • v) := by
      -- For each $a \in s$, the kernel of $f - aI$ is a subspace of $G$. Since $G$ is finite-dimensional, this subspace has a basis.
      have h_basis_eigenspaces : ∀ a ∈ s, ∃ T_a : Set G, Submodule.span R T_a = LinearMap.ker (f - a • 1) := by
        exact fun a ha => ⟨ _, ( Submodule.span_eq ( LinearMap.ker ( f - a • 1 ) ) ) ⟩;
      -- For each $a \in s$, the basis $T_a$ of $\ker(f - aI)$ satisfies $f(v) = a \cdot v$ for all $v \in T_a$ by definition of the kernel.
      intros a ha
      obtain ⟨T_a, hT_a⟩ := h_basis_eigenspaces a ha
      use T_a
      aesop;
      have := hT_a ▸ Submodule.subset_span a_1; simp_all ( config := { decide := Bool.true } ) [ sub_eq_zero ] ;
    choose! T hT using h_basis_eigenspaces;
    refine' ⟨ ⋃ a ∈ s, T a, _, _ ⟩ <;> simp_all ( config := { decide := Bool.true } ) [ Submodule.span_iUnion ];
    exact fun v a ha hv => ⟨ a, ha, hT a ha |>.2 v hv ⟩;
  cases' exists_linearIndependent R T with b hb;
  -- Since the vectors in $b$ are eigenvectors of $f$, we can define an eigenbasis using $b$.
  have hb_eigenbasis : ∃ B : Basis b R G, ∀ v : b, ∃ a ∈ s, f (B v) = a • B v := by
    refine' ⟨ _, _ ⟩;
    exact Basis.mk hb.2.2 ( by simp ( config := { decide := Bool.true } ) [ hb.2.1, hT.1 ] );
    aesop;
  obtain ⟨ B, hB ⟩ := hb_eigenbasis;
  use b;
  choose a ha using hB;
  refine' ⟨ _, _, _ ⟩;
  exact B;
  exacts [ fun _ => a, fun _ i => ha i |>.2 ]