-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
⊢ 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))
have dsimp : (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) sorry))
        (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 sorry)) (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))
Tactic: dsimp [shiftFunctorOpIso]