-- 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)
          (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)))
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).op.obj x ⟶ (F ⋙ shiftFunctor D (a + b)).op.obj x)
    (NatTrans.app (Iso.hom (Iso.symm (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))))) x)
    (NatTrans.app
      (Iso.hom (CommShift.isoAdd (Iso.symm (NatIso.op (commShiftIso F a))) (Iso.symm (NatIso.op (commShiftIso F b)))))
      x)

Tactic:
simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
      CommShift.isoAdd_inv_app, op_comp, Category.assoc, CommShift.isoAdd_hom_app]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.CommShift.isoAdd_inv_app, CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Iso.symm_hom, CategoryTheory.NatTrans.op_app, CategoryTheory.NatIso.op_inv, CategoryTheory.Functor.op_obj