chore(Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean): automated extraction (#38010)

This PR was automatically created from PR #37987 by @yuanyi-350 via a [review comment](#37987 (comment)) by @themathqueen.

Co-authored-by: yuanyi-350 <174429902+yuanyi-350@users.noreply.github.com>

Author: mathlib-splicebot[bot]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean

@@ -42,15 +42,12 @@ lemma cfcₙ_map_pi (f : R → R) (a : ∀ i, A i)
     (hf : ContinuousOn f (⋃ i, quasispectrum R (a i)) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) (ha' : ∀ i, q i (a i) := by cfc_tac) :
     cfcₙ f a = fun i => cfcₙ f (a i) := by
-  cases isEmpty_or_nonempty ι with
-  | inr h =>
-    by_cases hf₀ : f 0 = 0
-    · ext i
-      let φ := Pi.evalNonUnitalStarAlgHom S A i
-      exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)
-    · simp only [cfcₙ_apply_of_not_map_zero _ hf₀, Pi.zero_def]
-  | inl h =>
-    exact Subsingleton.elim _ _
+  by_cases hf₀ : f 0 = 0
+  · ext i
+    have : Nonempty ι := ⟨i⟩
+    let φ := Pi.evalNonUnitalStarAlgHom S A i
+    exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)
+  · simp only [cfcₙ_apply_of_not_map_zero _ hf₀, Pi.zero_def]
 
 end nonunital_pi