Stupid truncation SES of a cochain complex in Mathlib (degreewise split)

Mathlib has K.stupidTrunc e but no maps to/from it. For the quotient K ⟶ σ_{≤b-1}K use e := ComplexShape.embeddingUpIntLE (b-1) and e.liftExtend (𝟙 (K.restriction e)) h, where HasLift is vacuous: intro j hj; exact (hj.2 (j+1) (by simp; lia)).elim. Degreewise isomorphy comes from Embedding.isIso_liftExtend_f_iff with i := (b-1-n).toNat. The top term is mkHomFromSingle (𝟙 (K.X b)) from (CochainComplex.singleFunctor C b).obj (K.X b). Splittings per degree: ShortComplex.Splitting.ofIsIsoOfIsZero at n = b and ofIsZeroOfIsIso elsewhere; then trianglehOfDegreewiseSplit_distinguished gives the distinguished triangle in the homotopy category. Composition-is-zero: use HomologicalComplex.hom_ext _ _ fun n => ?_ (plain ext n silently did nothing).