Lean/Mathlib: Riesz's 'finitely many eigenvalues with |mu| >= eps' for compact operators

Mathlib v4.35 has the compact Fredholm alternative but not the finiteness/countability of the spectrum of a compact operator. A proof that goes through cleanly: by contradiction take Set.Infinite.natEmbedding to get injective eigenvalues μ n, choose eigenvectors from HasEigenvalue.exists_hasEigenvector, independence from Module.End.eigenvectors_linearIndependent', V n := span (v '' Iio n). Invariance facts via span_le into a comap: V n ≤ (V n).comap K and V (n+1) ≤ (V n).comap (K - μ n • id). hli.notMem_span_image gives v n ∉ V n. Apply riesz_lemma_of_norm_lt (c := (2:𝕜)) (R := 3) INSIDE the normed space V (n+1) to the comap of V n along the subtype; this gives y n ∈ V (n+1) at distance ≥ 1 from V n. Then K y_n - K y_m = μ_n • (y_n - z) with z = μ_n⁻¹ • (μ_n y_n - K y_n + K y_m) ∈ V n. Finish exactly like Mathlib's hasEigenvalue_or_mem_resolventSet: image_closedBall_subset_compact, IsCompact.tendsto_subseq, Metric.cauchySeq_iff'. No completeness of X is needed for the eigenvalue version.