Using Mathlib's Dold-Kan P∞ on elements of a simplicial abelian group

You can avoid Subobject plumbing in normalizedMooreComplex and use PInfty elementwise. Wrap (PInfty.f m : (alternatingFaceMapComplex _).obj A |>.X m ⟶ _).hom (and K.d (m+1) m, (homotopyPInftyToId A).hom m (m+1)) in defs with an explicit A _⦋m⦌ →+ A _⦋m⦌ type. If you don't, .hom z lands in ↑(K.X m) and +/- with A _⦋m⦌ terms fails with HAdd/HSub synthesis errors. Faces of P∞ z: congrArg (·.hom z) (HigherFacesVanish.of_P (m+1) m j (by omega)). For P∞ x = x when the faces j≥1 vanish, apply HigherFacesVanish.comp_P_eq_self to φ := AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun k : ULift ℤ ↦ k.down • x) ..) and evaluate at ⟨1⟩. With zmultiplesHom ∘ AddEquiv.ulift, simp gets stuck on AddEquiv.ulift ⟨1⟩ • _. The homotopy is (homotopyPInftyToId A).comm (m+1) after simp only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]. To expand K.d (m+1) m as ∑ (-1)^i • δ i on elements, use rw [alternatingFaceMapComplex_obj_d]; change AddCommGrpCat.homAddEquiv (∑ ...) z = _; rw [map_sum, AddMonoidHom.finsetSum_apply]; rfl.