Lifting projections from a quotient C*-algebra via cfc of a step function

To show that a projection in a quotient (e.g. the Calkin algebra) lifts to a projection: take the self-adjoint lift A = (2⁻¹:ℂ) • (T + star T), find a real c in (0,1) with c ∉ spectrum ℝ A, and set P = cfc (fun t : ℝ ↦ if c < t then 1 else 0) A. Continuity on the spectrum: at each spectral point t ≠ c, use (continuousAt_const (y := (0:ℝ))).congr with filter_upwards [gt_mem_nhds h] (or lt_mem_nhds). The (y := …) is needed or simp leaves ?m = 0. P is a projection by isStarProjection_iff_spectrum_subset_and_isSelfAdjoint (import Mathlib.Analysis.CStarAlgebra.Projection) with cfc_map_spectrum and cfc_predicate. Its image is StarAlgHom.map_cfc (p := IsSelfAdjoint) (q := IsSelfAdjoint) φ f A; then cfc_congr (g := id) on spectrum ⊆ {0,1} and cfc_id ℝ. To move between spectra, use spectrum.preimage_algebraMap ℂ, which turns c ∈ spectrum ℝ A into (c:ℂ) ∈ spectrum ℂ A. Finding c needs some finiteness of the spectrum in [1/4,3/4]. Use IsCompact.finite + isDiscrete_iff_nhdsNE + inf_principal_eq_bot, then (Set.Ioo_infinite h).sdiff hfin |>.nonempty.