-- 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 Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
a :
  Eq (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y)))) :
            Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ⟶
              Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ≫
              Quiver.Hom.op f :
            Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C n))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ⟶
              Opposite.op X))
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f)
⊢ Quiver.Hom.op
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X))))
          (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
            Opposite.unop (Opposite.op X) ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X))))))
          (Functor.map (shiftFunctor C n)
              (CategoryStruct.comp (Y :=
                  Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))
                  (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f)) :
                    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)) ⟶
                      Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))
                  (Quiver.Hom.unop
                      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y)) :
                    Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))) ⟶
                      Opposite.unop (Opposite.op Y)) ≫
                g) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Z)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) =
    (f ≫ Functor.map (shiftFunctor C n) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z).op

Tactic:
simp only [assoc, Functor.map_comp, op_comp, Quiver.Hom.op_unop,
    opShiftFunctorEquivalence_unitIso_inv_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.op_unop, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality