chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq (#36106)

Use proof by cases to remove an unnecessary hypothesis from `LinearMap.IsSymmetric.card_filter_eigenvalues_eq` and the related private `LinearMap.IsSymmetric.card_filter_unsortedEigenvalues_eq`. This required proving a statement similar to `LinearMap.IsSymmetric.hasEigenvalue_eigenvalues` but for `unsortedEigenvalues`.

Author: nielsvoss

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -205,6 +205,13 @@ private noncomputable def unsortedEigenvalues (hT : T.IsSymmetric) (hn : Module.
   @RCLike.re 𝕜 _ <| (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
     hT.orthogonalFamily_eigenspaces').val
 
+private theorem hasEigenvalue_unsortedEigenvalues (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
+    (i : Fin n) : HasEigenvalue T (hT.unsortedEigenvalues hn i) := by
+  unfold unsortedEigenvalues
+  let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
+    hT.orthogonalFamily_eigenspaces'
+  rwa [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]
+
 private theorem exists_unsortedEigenvalues_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
     {μ : 𝕜} (hμ : HasEigenvalue T μ) : ∃ i : Fin n, hT.unsortedEigenvalues hn i = μ := by
   let (eq := hx) x : Eigenvalues T := ⟨μ, hμ⟩
@@ -215,15 +222,19 @@ private theorem exists_unsortedEigenvalues_eq (hT : T.IsSymmetric) (hn : Module.
     hT.conj_eigenvalue_eq_self hμ]
 
 private theorem card_filter_unsortedEigenvalues_eq (hT : T.IsSymmetric)
-    (hn : Module.finrank 𝕜 E = n) {μ : 𝕜} (hμ : HasEigenvalue T μ) :
+    (hn : Module.finrank 𝕜 E = n) (μ : 𝕜) :
     Finset.card {i | hT.unsortedEigenvalues hn i = μ} = Module.finrank 𝕜 (eigenspace T μ) := by
-  convert hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
-    hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i
-  rw [unsortedEigenvalues]
-  set x := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
-    hT.orthogonalFamily_eigenspaces'
-  rw [RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self (μ := x.val) x.property)]
-  aesop
+  by_cases hμ : HasEigenvalue T μ
+  · convert hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
+      hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i
+    unfold unsortedEigenvalues
+    let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
+      hT.orthogonalFamily_eigenspaces'
+    rw [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]
+    exact Subtype.mk_eq_mk.symm
+  · rw [Module.End.hasEigenvalue_iff.not_left.mp hμ, finrank_bot, Finset.card_filter_eq_zero_iff]
+    intro i _ rfl
+    exact hμ (hT.hasEigenvalue_unsortedEigenvalues hn i)
 
 private noncomputable def unsortedEigenvectorBasis (hT : T.IsSymmetric)
     (hn : Module.finrank 𝕜 E = n) : OrthonormalBasis (Fin n) 𝕜 E :=
@@ -265,10 +276,9 @@ theorem exists_eigenvalues_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E =
   use ((Tuple.sort (hT.unsortedEigenvalues hn)).symm i).revPerm
   simp [eigenvalues_def, hi]
 
-theorem card_filter_eigenvalues_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {μ : 𝕜}
-    (hμ : HasEigenvalue T μ) :
+theorem card_filter_eigenvalues_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (μ : 𝕜) :
     Finset.card {i | hT.eigenvalues hn i = μ} = Module.finrank 𝕜 (eigenspace T μ) := by
-  rw [← hT.card_filter_unsortedEigenvalues_eq hn hμ, eigenvalues_def]
+  rw [← hT.card_filter_unsortedEigenvalues_eq hn, eigenvalues_def]
   apply Finset.card_equiv (Fin.revPerm.trans (Tuple.sort (hT.unsortedEigenvalues hn)))
   simp