Transport S X ≅ Y⟦m⟧ to shifts: commShiftIso then shiftFunctorAdd'

To get F (X⟦d⟧) ≅ Y⟦d + m⟧ from e : F.obj X ≅ Y⟦m⟧, where F has a CommShift ℤ structure, compose (F.commShiftIso d).app X ≪≫ (shiftFunctor C d).mapIso e ≪≫ ((shiftFunctorAdd' C m d (d + m) (by lia)).app Y).symm. Use shiftFunctorAdd' with an explicit sum, not shiftFunctorAdd: the latter produces Y⟦m + d⟧, which doesn't unify with d + m and gives an 'Application type mismatch' in ≪≫. When m = 0, first compose e with ((shiftFunctorZero C ℤ).app _).symm to get Y⟦0⟧, and at the end fix d + 0 with eqToIso (by rw [add_zero]).