-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X))) =
    CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
        (Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
          (CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
              (CategoryStruct.comp (Y :=
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                      (Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
                  (Functor.map (shiftFunctor C p)
                      (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorAdd' Cᵒᵖ n m p ⋯)) X)) ≫
                    NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
                      (Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
                  (Functor.map (shiftFunctor C n)
                    (Quiver.Hom.unop
                      (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C m)))
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X)) ⟶
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
              (Functor.map (shiftFunctor C n)
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m)))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)) ⟶
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                      (Opposite.unop
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n)
                (Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
                (Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X)) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
            (Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (Functor.map (shiftFunctor C p) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ n m p ⋯)) X)) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
            (Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C p)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ p) X)))

Tactic:
simp only [Category.assoc,
    ← unop_comp, Iso.inv_hom_id_app, Functor.comp_obj, Functor.op_obj, unop_id,
    Functor.map_id, id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.unop_comp, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.op_obj, CategoryTheory.unop_id, CategoryTheory.Category.id_comp