-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
simp :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X))))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)))
          (map (shiftFunctor D n)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
            map (shiftFunctor D n)
                (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
    (F.map
        (map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (unop X)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
        F.obj (unop X))
    (CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
        (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
        (CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))))
          (map (shiftFunctor D n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso F.op n)) X)) :
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
                (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
              obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
                (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))))
          (map (shiftFunctor D n)
                (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
                (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))) ⟶
              F.obj (unop X))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
        F.obj (unop X))

Tactic:
simp only [map_comp, unop_comp, Quiver.Hom.unop_op, assoc,
    map_shiftFunctorCompIsoId_hom_app, commShiftIso_hom_naturality_assoc,
    op_commShiftIso_inv_app _ _ _ _ (add_neg_cancel n)]

Premises used: CategoryTheory.Category.assoc, add_neg_cancel, Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Functor.commShiftIso_hom_naturality_assoc, CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app, CategoryTheory.Functor.op_commShiftIso_inv_app, CategoryTheory.Functor.map_comp