-- 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 ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p))
          X) ⟶
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p))
          X))
    (Quiver.Hom.unop
      (𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C p) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C p))
          X)))
    (Quiver.Hom.unop
      (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))))))))
have a : 𝟙
    (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 sorry)) 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 sorry)) 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: dsimp