-- 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
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p)) X)
    (𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p)) X))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (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ᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X))))
      (Quiver.Hom.op
        (Functor.map (shiftFunctor C p) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ n m p ⋯)) X))))
      (Quiver.Hom.op
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (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} (𝟭 Cᵒᵖ) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
          (Quiver.Hom.op
            (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)))))
          (CategoryStruct.comp (Y :=
            Opposite.op
              (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}
                    (Equivalence.functor (opShiftFunctorEquivalence C m) ⋙
                      Equivalence.inverse (opShiftFunctorEquivalence C m))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
            (Quiver.Hom.op
              (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)))))
            (Quiver.Hom.op
                (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (opShiftFunctorEquivalence C m))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) ≫
              Quiver.Hom.op
                (Functor.map (shiftFunctor C p)
                  (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorAdd' Cᵒᵖ n m p ⋯)) X)))))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C p))) X)
    (CategoryStruct.comp (Y :=
      Opposite.op
        (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ᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X))))
      (Quiver.Hom.op
        (Functor.map (shiftFunctor C p) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ n m p ⋯)) X))))
      (Quiver.Hom.op
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m) X))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (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} (𝟭 Cᵒᵖ) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
          (Quiver.Hom.op
              (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)))) :
            Opposite.op
                (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}
                      (Equivalence.functor (opShiftFunctorEquivalence C m) ⋙
                        Equivalence.inverse (opShiftFunctorEquivalence C m))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))) ⟶
              Opposite.op
                (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} (𝟭 Cᵒᵖ)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X :
            Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C n))
                X ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)))

Tactic:
rw [← cancel_mono ((opShiftFunctorEquivalence C p).unitIso.hom.app X), Iso.inv_hom_id_app,
    opShiftFunctorEquivalence_add_unitIso_hom_app_eq _ _ _ _ h,
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, CategoryTheory.Category.assoc, CategoryTheory.Equivalence.unitIso, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.NatTrans.app