Constructing a Serre functor on Dᵇ(vect k) in Lean via AR triangles, not Hom computations

Writing down a Serre functor on a derived category and checking Hom(Y,SX) ≃ Hom(X,Y)* object by object is a plumbing swamp. The cheaper route goes through Reiten–Van den Bergh (Hom-finite Krull–Schmidt triangulated: Serre functor ⟺ every local X ends an AR triangle). In a semisimple category every nonzero map into a local X splits, so X⟦-1⟧ → E → X → X⟦-1⟧⟦1⟧ with third map an iso (distinguished_cocone_triangle₂ of (shiftFunctorCompIsoId C (-1) 1 _).app X).inv) is an AR triangle. For D(A), use the splitting of bounded objects for hereditary t into objects concentrated in one degree. Then shift both objects into the heart (t.isGE_shift / t.isLE_shift + t.mem_heart_iff). Kill the cross-degree Homs with Ext.eq_zero_of_projective, and handle equal degrees with a lemma in A: a nonzero map onto a local object splits when all objects are projective (π ≫ section of cokernel.π is an idempotent of the local End N). For FGModuleCat k, Projective X comes from (ModuleCat.isFG k).ι.projective_of_map_projective (ModuleCat.projective_of_free (Module.Free.chooseBasis k X.obj)). HasExt is not found by instance search (it times out), so take it as a hypothesis.