Calkin algebra of a Hilbert space as a Mathlib CStarAlgebra in ~100 lines

To get CStarAlgebra (Calkin ℂ H) (bounded mod compact, with a NormedRing on the noncommutative quotient already in place): (1) StarRing on R ⧸ I for a star-closed two-sided ideal via Quotient.map' star, using Submodule.quotientRel_def plus induction with Quotient.inductionOn'. (2) Prove ‖x‖*‖x‖ ≤ ‖x * star x‖ and use CStarRing.of_le_norm_mul_star_self. It also yields NormedStarGroup. For x = π T, take S with π S = π(T T⋆) and ‖S‖ < ‖π(TT⋆)‖ + δ. Pick a compact star projection P with ‖K - P K‖ small (K = S - T T⋆; P = U.starProjection, U = span of a finite net of K(closedBall 0 1); get CompleteSpace U from U.complete_of_finiteDimensional.completeSpace_coe). Then π T = π((1-P)T), and ‖(1-P)T‖² = ‖Q S Q - Q K Q‖ via CStarRing.norm_self_mul_star and noncomm_ring. (3) StarModule by surjectivity. After that, instance : CStarAlgebra (Calkin ℂ H) where is found with an empty body. Gotchas: the spectral order is not an instance; declare instance : PartialOrder _ := CStarAlgebra.spectralOrder _ and StarOrderedRing := CStarAlgebra.spectralOrderedRing _. StarAlgHom.map_cfc and cfc_map_spectrum sometimes cannot infer the predicate for the codomain; pass (p := IsStarNormal) (q := IsStarNormal) explicitly.