-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.OpOp (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
p q : ℤ
X : Cᵒᵖᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (p + q) ⋙ unopUnop C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C (p + q)) X)
    (NatTrans.app (Iso.hom (iso C (p + q))) X) (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (iso C p) (iso C q))) X)
have w : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (p + q) ⋙ unopUnop C) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C ⋙ shiftFunctor C (p + q)) X)
  (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ (p + q) (-(p + q)) sorry)) X)) ≫
      Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-(p + q)) (p + q) sorry)) (unop X)) :
    unop (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (p + q)) X)) ⟶
      unop (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (p + q))) (unop X)))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ p ⋙ shiftFunctor Cᵒᵖᵒᵖ q) X))
      (Functor.map (unopUnop C) (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ (p + q) (-(p + q)) sorry)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C)
            (op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-p) ⋙ shiftFunctor Cᵒᵖ (-q)) (unop X))))
          (((Functor.map (unopUnop C)
                  (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-(p + q)) (p + q) sorry)) (unop X))) ≫
                Functor.map (unopUnop C)
                  (Quiver.Hom.op
                    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C p q (p + q) sorry)) (unop (unop X)))))) ≫
              Functor.map (unopUnop C)
                (Quiver.Hom.op
                  (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-q) q sorry))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C p)) (unop X))))) ≫
            (Functor.map (unopUnop C)
                  (Quiver.Hom.op
                    (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-q) q sorry))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C p)) (unop X)))) ≫
                Functor.map (unopUnop C)
                  (Quiver.Hom.op
                    (Quiver.Hom.op
                      (Functor.map (shiftFunctor C q)
                        (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-p) p sorry)) (unop X))))))) ≫
              Functor.map (unopUnop C)
                (Quiver.Hom.op
                  (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-q) q sorry))
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-p)) (unop X)))))
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C)
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ q)
                (op ((shiftFunctor Cᵒᵖ (-p) : Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ).1 (unop X)))))
            (Functor.map (unopUnop C)
              (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ q (-q) sorry))
                (op ((shiftFunctor Cᵒᵖ (-p) : Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ).1 (unop X)))))
            (Functor.map (unopUnop C)
                (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ q (-q) sorry))
                  (op ((shiftFunctor Cᵒᵖ (-p) : Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ).1 (unop X)))) ≫
              ((Functor.map (unopUnop C)
                      (Quiver.Hom.op
                        (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-q) q sorry))
                          ((shiftFunctor Cᵒᵖ (-p) : Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ).1 (unop X)))) ≫
                    Functor.map (unopUnop C)
                      (Quiver.Hom.op
                        (Quiver.Hom.op
                          (Functor.map (shiftFunctor C q)
                            (Quiver.Hom.unop
                              (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ p (-p) sorry)) X))))))) ≫
                  Functor.map (unopUnop C)
                    (Quiver.Hom.op
                      (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-q) q sorry))
                        (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ p) X))))) ≫
                Functor.map (unopUnop C)
                  (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ q (-q) sorry))
                    (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} (unopUnop C ⋙ shiftFunctor C q)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ p) X))
        (Quiver.Hom.unop
            (Quiver.Hom.unop
              (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ q (-q) sorry))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ p) X))) ≫
          Quiver.Hom.unop
            (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-q) q sorry))
              (unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ p) X))))
        ((Functor.map (shiftFunctor C q)
              (Quiver.Hom.unop (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso Cᵒᵖ p (-p) sorry)) X))) ≫
            Functor.map (shiftFunctor C q)
              (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-p) p sorry)) (unop X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C p q (p + q) sorry))
            (Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C) X))) :
    Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (p + q)) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (p + q)) (Functor.obj.{v_1, v_1, u_1, u_1} (unopUnop C) X))
Tactic: simp only [Functor.CommShift.isoAdd_hom_app, op_comp,
      ← shiftFunctorAdd'_eq_shiftFunctorAdd, Functor.map_comp,
      fun X n ↦ iso_hom_app X n (-n) (add_neg_cancel n),
      shiftFunctorAdd'_op_hom_app _ p q (p + q) rfl (-p) (-q) (-(p + q))
        (add_neg_cancel p) (add_neg_cancel q) (add_neg_cancel (p + q)),
      shiftFunctorAdd'_op_inv_app _ (-p) (-q) (-(p + q)) (by lia) p q (p + q)
        (neg_add_cancel p) (neg_add_cancel q) (neg_add_cancel (p + q)),
      shiftFunctor_op_map _ (-q) q, shiftFunctor_op_map _ q (-q)]