Calkin algebra in Mathlib: TwoSidedIdeal.mk' + RingCon quotient gives the algebra free

To get the Calkin algebra (bounded mod compact operators) as a 𝕜-algebra with minimal work: define the ideal with TwoSidedIdeal.mk' {T | IsCompactOperator T} isCompactOperator_zero (·.add ·) (·.neg) (fun {x _} hy ↦ hy.clm_comp x) (fun {_ y} hx ↦ hx.comp_clm y) (multiplication in E →L E is composition), then abbrev Calkin := I.ringCon.Quotient — RingCon.Quotient already has Ring and Algebra α instances, and RingCon.mkₐ 𝕜 _ is the quotient AlgHom. Useful facts: RingCon.eq + TwoSidedIdeal.rel_iff give π S = π T ↔ S - T ∈ I; TwoSidedIdeal.mem_mk' unfolds membership; surjectivity is Quotient.mk''_surjective. Spectrum in the quotient (essential spectrum) then works with spectrum.mem_iff, map_sub, AlgHom.commutes, and AlgHom.spectrum_apply_subset. A well-defined map out of the units (e.g. the Fredholm index) can be built with MonoidHom.mk' on a choosen lift plus a lemma that any lift gives the same value.