-- 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 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
a b : A
x : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (obj
            (OppositeShift.functor A F :
              Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (Quiver.Hom.unop
            (map (OppositeShift.functor A F) (NatTrans.app (Iso.inv (shiftFunctorAdd Cᵒᵖ a b)) (Opposite.op x))) :
          Opposite.unop (Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x))) ⟶
            Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (CategoryStruct.comp (Y :=
            Opposite.unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                (obj
                  (OppositeShift.functor A F :
                    Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                      (OppositeShift.{v_2, u_2, u_3} D A))
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x))))
            (CategoryStruct.comp (Y :=
              Opposite.unop
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ a)
                    (obj
                      (OppositeShift.functor A F :
                        Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                          (OppositeShift.{v_2, u_2, u_3} D A))
                      (Opposite.op x)))))
              (Quiver.Hom.unop
                (map (shiftFunctor Dᵒᵖ b)
                  (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.hom (shiftFunctorAdd Dᵒᵖ a b))
                  (obj
                    (OppositeShift.functor A F :
                      Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                        (OppositeShift.{v_2, u_2, u_3} D A))
                    (Opposite.op x))))) :
          Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) x) ≫
        CategoryStruct.comp (Y :=
          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) x)))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
              (Opposite.op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) x))))
          (map (shiftFunctor D b)
              (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
⊢ Eq.{v_2 + 1} (α := (shiftFunctor C (a + b) ⋙ F).obj x ⟶ (F ⋙ shiftFunctor D (a + b)).obj x)
    (NatTrans.app
      (Iso.hom
        (NatIso.removeOp
          (Iso.symm
            (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
              (commShiftIso (OppositeShift.functor A F) b)))))
      x)
    (NatTrans.app
      (Iso.hom
        (CommShift.isoAdd (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) a)))
          (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) b)))))
      x)

Tactic:
simp only [comp_obj, NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app, op_obj,
      CommShift.isoAdd_inv_app, unop_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.Iso.symm_hom, CategoryTheory.unop_comp, CategoryTheory.NatIso.removeOp_hom, CategoryTheory.NatTrans.removeOp_app, CategoryTheory.Functor.op_obj