-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a b : A
x : Cᵒᵖ
w :
  Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
              (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x)))))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x))))
          (Quiver.Hom.op (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj (Opposite.unop x)))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
            (obj (OppositeShift.functor A F)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x)))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b))
              (Opposite.unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x))))
          (map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
              (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op
              (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (Opposite.unop (obj (OppositeShift.functor A F) x)))) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b)) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b))
          (obj (OppositeShift.functor A F) x)))
⊢ Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
              (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x)))))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x))))
          (Quiver.Hom.op (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj (Opposite.unop x)))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (NatTrans.app (Iso.hom (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_3} C A) a b)) x) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
            (obj (OppositeShift.functor A F)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x)))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b))
              (Opposite.unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x))))
          (map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
              (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd (OppositeShift.{v_2, u_2, u_3} D A) a b))
              (obj (OppositeShift.functor A F) x)) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b)) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b))
          (obj (OppositeShift.functor A F) x)))

Tactic:
erw [oppositeShiftFunctorAdd_inv_app, oppositeShiftFunctorAdd_hom_app]

Premises used: CategoryTheory.oppositeShiftFunctorAdd_inv_app, CategoryTheory.oppositeShiftFunctorAdd_hom_app