-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
dsimp :
  Eq (α := ShiftedHom Y Z c)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)) :
          Opposite.unop (Opposite.op Y) ⟶
            Opposite.unop
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      Functor.map (shiftFunctor C a) z ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)) :
          Opposite.unop (Opposite.op Y) ⟶
            Opposite.unop
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f ≫ z) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
⊢ Eq (α := ShiftedHom Y Z c)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
            (Opposite.op Y)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f)) ≫
      Functor.map (shiftFunctor C a) z ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
            (Opposite.op Y)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop (Quiver.Hom.op z ≫ f))) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)

Tactic:
dsimp