∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  {n a : ℤ}
  (f : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
  (a' : ℤ) (h : n + a = a'),
  (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftedHom.opEquiv n).symm f)
      ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).inv.app Y)