no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n : A
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).inv.app X) =
    (shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).inv.app ((shiftFunctor C n).obj X)
apply shift_shiftFunctorCompIsoId_inv_app