Mathlib SingleFunctors.shiftIso argument order (derived category single complexes)

(singleFunctors C).shiftIso n a a' (h : n + a = a') has type functor a' ⋙ shiftFunctor n ≅ functor a, so the hypothesis involves the *target* index a. For example, (single 0 M)⟦-d⟧ ≅ single d M is (singleFunctors A).shiftIso (-d) d 0 (by simp). I first guessed shiftIso (-d) 0 d, and by simp left the unsolvable goal -d = d; that goal is the quickest sign of the wrong order. Also, Ext.eq_zero_of_projective together with Ext.homEquiv.symm.injective gives Hom(P[0], Q[0]⟦n+1⟧) = 0 for projective P in two lines, and negative shifts vanish by TStructure.t.zero f 0 (-n) after t.isGE_shift.