-- 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 : ℤ
rw :
  Eq (α := F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)) ⟶ F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)))
    (F.map (Quiver.Hom.unop (𝟙 (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))))
    (CategoryStruct.comp (Y :=
      unop
        (obj.{v_2, v_2, u_2, u_2}
          (Equivalence.functor (opShiftFunctorEquivalence D n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence D n))
          (op (F.obj (unop X)))))
      (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
      (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)))
        (map (shiftFunctor D n)
            (Quiver.Hom.unop
              (CategoryStruct.comp (Y := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
                (NatTrans.app (Iso.inv (commShiftIso F.op n)) X) (NatTrans.app (Iso.hom (commShiftIso F.op n)) X))) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
              (unop
                (obj.{v_2, v_2, u_2, u_2} (Equivalence.functor (opShiftFunctorEquivalence D n))
                  (op (F.obj (unop X))))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
          unop
              (obj.{v_2, v_2, u_2, u_2}
                (Equivalence.functor (opShiftFunctorEquivalence D n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence D n))
                (op (F.obj (unop X)))) ⟶
            unop (obj.{v_2, v_2, u_2, u_2} (𝟭 Dᵒᵖ) (op (F.obj (unop X)))))))
⊢ Eq (α :=
    F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)) ⟶
      F.obj
        (unop
          (obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            X)))
    (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)))
    (CategoryStruct.comp (Y :=
      unop
        (obj.{v_2, v_2, u_2, u_2}
          (Equivalence.functor (opShiftFunctorEquivalence D n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence D n))
          (op (F.obj (unop X)))))
      (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
      (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)))
        (map (shiftFunctor D n) (Quiver.Hom.unop (NatTrans.app (Iso.hom (commShiftIso F.op n)) X)))
        (NatTrans.app (Iso.inv (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))

Tactic:
rw [← cancel_mono (F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop),
    ← F.map_comp, ← unop_comp, Iso.hom_inv_id_app,
    map_opShiftFunctorEquivalence_unitIso_hom_app_unop, assoc, assoc,
    Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc, ← unop_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Equivalence.unitIso, Quiver.Hom.unop, CategoryTheory.unop_comp, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.NatTrans.app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop