-- 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} (α :=
    X ⟶
      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ᵒᵖ p) X))))
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-p) p ⋯)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C p) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C p (-p) ⋯)) X))))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (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 (-n)) (Opposite.unop X))))
      (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 (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (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))))))
          (Quiver.Hom.op
            (Functor.map (shiftFunctor C n)
              (Functor.map (shiftFunctor C m)
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (shiftFunctorOpIso C m (-m) ⋯))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ≫
                NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m ⋯))
                  (Opposite.unop (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} (shiftFunctor 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.hom (shiftFunctorOpIso C m (-m) ⋯))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ≫
                    Quiver.Hom.op
                        (Functor.map (shiftFunctor C (-m))
                          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
                      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) ⋯)) (Opposite.unop X)) ≫
                        NatTrans.app (Iso.inv (shiftFunctorOpIso C p (-p) ⋯)) X))))))
have erw : Eq.{v_1 + 1} (α :=
  X ⟶
    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ᵒᵖ p) X))))
  (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-p) p sorry)) (Opposite.unop X)))
  (CategoryStruct.comp (Y :=
    Opposite.op
      (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 (-n)) (Opposite.unop X))))
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n sorry)) (Opposite.unop X)))
    (CategoryStruct.comp (Y :=
      Opposite.op
        (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))))))
      (Quiver.Hom.op
        (Functor.map (shiftFunctor C n)
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-m) m sorry))
            (Opposite.unop (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} (shiftFunctor 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
              (Quiver.Hom.op
                  (𝟙
                    (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} (Functor.op (shiftFunctor C (-n))) X)))) ≫
                Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C (-n) (-m) (-p) sorry)) (Opposite.unop X))))))))
Tactic: erw [Functor.map_id, Functor.map_id, Functor.map_id, Functor.map_id,
    id_comp, id_comp, id_comp, comp_id, comp_id]