-- 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
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
rw :
  Eq.{v_1 + 1} (α := ShiftedHom X Z c)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (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)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
          (Functor.map (shiftFunctor C b)
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (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)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
          (Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ a) g)) ≫
              Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (Quiver.Hom.unop f) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯)) Z :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b)
                (Opposite.unop
                  (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) (Opposite.op X)))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
      (Functor.map (shiftFunctor C b) (Quiver.Hom.unop g) ≫
          Functor.map (shiftFunctor C b)
              (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))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯)) Z :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
⊢ Eq.{v_1 + 1} (α := ShiftedHom X Z c)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
        Opposite.unop (Opposite.op X) ⟶
          Opposite.unop
            (Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (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)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
          (Functor.map (shiftFunctor C b)
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X)))) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (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)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯))
                (Opposite.unop
                  (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) (Opposite.op X)))) ≫
              Functor.map (shiftFunctor C c)
                (𝟙
                    (Opposite.unop
                      (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) (Opposite.op X)))) ≫
                  Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ a) g) ≫ Quiver.Hom.unop f) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (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)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y)
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))
          (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)) :
            Opposite.unop (Opposite.op X) ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))))
          (Functor.map (shiftFunctor C b) (Quiver.Hom.unop g) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y) :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y)
      (Functor.map (shiftFunctor C b)
            ((Equiv.symm (opEquiv a) : (a_1 : ShiftedHom (Opposite.op Z) (Opposite.op Y) a) → ShiftedHom Y Z a) f) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c ⋯)) Z :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))

Tactic:
rw [assoc, id_comp, Functor.map_comp, ← NatTrans.naturality_assoc,
    ← NatTrans.naturality, opEquiv_symm_apply]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.ShiftedHom.opEquiv_symm_apply, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp