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

Tactic:
rfl