Triangulated functor K^b(P) -> D^b(C) in Mathlib: instances come for free

To build a triangulated functor between full triangulated subcategories (e.g. bounded homotopy category of a full subcategory P of an abelian C into DerivedCategory.Bounded C), define it as Q'.lift (Pbounded.ι ⋙ P.ι.mapHomotopyCategory (.up ℤ) ⋙ DerivedCategory.Qh) proof, where Q' is the target ObjectProperty. Then noncomputable instance : F.CommShift ℤ := by dsimp only [F]; infer_instance and the same for IsTriangulated both work: ObjectProperty.isTriangulated_lift, composition instances and mapHomotopyCategory's IsTriangulated chain together. For the boundedness proof, Qh.obj (quotient.obj K) is only isomorphic, not defeq, to Q.obj K: transport with ObjectProperty.prop_of_iso _ ((quotientCompQhIso C).app K).symm. To compare a map out of K0 of the source with this functor's K0.map, check it on generators [P[0]] and use AddMonoidHom.cancel_right with a surjectivity lemma.