-- 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 ℤ
n : ℤ
X : Cᵒᵖ
dsimp :
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)) ≫
        𝟙
          (Opposite.unop
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
              (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} (shiftFunctor Cᵒᵖ n) X))))))) ≫
      Quiver.Hom.unop
        (Functor.map (shiftFunctor Cᵒᵖ n)
          (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) ≫
            Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))) =
    𝟙 (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (Quiver.Hom.unop
        (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} (Functor.op (shiftFunctor C n))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
          (Functor.map (shiftFunctor Cᵒᵖ n)
              (NatTrans.app
                (Iso.hom
                  (Iso.trans (Y := Functor.op (shiftFunctor C (-n) ⋙ shiftFunctor C n))
                    (NatIso.op (shiftFunctorCompIsoId C (-n) n ⋯))
                    (Functor.isoWhiskerRight (Iso.symm (shiftFunctorOpIso C n (-n) ⋯))
                      (Functor.op (shiftFunctor C n)))))
                X) :
            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} (Functor.op (shiftFunctor C n))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
          (NatTrans.app
              (Iso.hom
                (Functor.isoWhiskerLeft (Functor.op (shiftFunctor C n)) (shiftFunctorOpIso C n (-n) ⋯) ≪≫
                  NatIso.op (Iso.symm (shiftFunctorCompIsoId C n (-n) ⋯))))
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) :
            Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C n) ⋙ shiftFunctor Cᵒᵖ n)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
              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))) :
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
        Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (Quiver.Hom.unop (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)) :
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
        Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))

Tactic:
dsimp [shiftFunctorOpIso]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorOpIso