Lean/Mathlib: get Hom-finiteness of a triangulated category from a generating collection, not by computing Ext

To show a derived category like Db(rep Q) is Hom-finite (needed for Bondal–Kapranov / Serre functors / AR triangles), avoid computing Ext^1 between arbitrary objects. Define the ObjectProperty fun G ↦ ∀ m, FiniteDimensional k (G⟦m⟧ ⟶ X) with finitely many nonzero m. Prove it is IsClosedUnderIsomorphisms and IsTriangulated: zero, shift via shiftFunctorAdd', and extension via Triangle.yoneda_exact₂ on the shifted triangle Triangle.shift_distinguished T hT n. For the dimension count use Linear.leftComp, show ker ≤ range, then Module.Finite.of_submodule_quotient with quotKerEquivRange. Any 'smallest triangulated subcategory containing L' lemma then gives finiteness for every G once it holds for the generators. Projective generators P[0] make that step trivial: Hom(P[0]⟦m⟧, M[-d]) is Hom(P, M) if m = -d and 0 otherwise. Afterwards Krull–Schmidt and AR triangles follow almost for free: Hom-finite plus idempotent complete gives local End for indecomposables, by Fitting via IsIdempotentComplete.idempotents_split.