-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
⊢ Eq (α := ShiftedHom X Y a'')
    ((CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n))
            (Opposite.unop
              (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.op X)))))
          (CategoryStruct.comp (Y :=
              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) (Opposite.op X))))
              (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X)) :
                Opposite.unop (Opposite.op X) ⟶
                  Opposite.unop
                    (Opposite.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} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
              (Functor.map (shiftFunctor C m)
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)))) :
                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) (Opposite.op X))) ⟶
                  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)
                      (Opposite.unop
                        (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.op X)))))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C n m (m + n) ⋯))
              (Opposite.unop
                (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.op X)))))
          (Functor.map (shiftFunctor C (m + n))
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯)) (Opposite.op X)))) ≫
        Functor.map (shiftFunctor C (m + n)) x.unop) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a (m + n) a'' ⋯)) Y)
    (CategoryStruct.comp (Y :=
        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) (Opposite.op X))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X)) :
          Opposite.unop (Opposite.op X) ⟶
            Opposite.unop
              (Opposite.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} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
        (Functor.map (shiftFunctor C m)
            (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)
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m)) X)))))
                (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m)) X))) :
                  Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)) ⟶
                    Opposite.unop
                      (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)
                              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m)) X)))))))
                (Functor.map (shiftFunctor C n)
                    (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd Cᵒᵖ m n)) (Opposite.op X)) ≫ x.unop) :
                  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)
                          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m)) 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 a) Y)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y) :
          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) (Opposite.op X))) ⟶
            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 a') Y)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a' m a'' ⋯)) Y)
have simp : Eq.{v_1 + 1} (α := ShiftedHom X Y a'')
  (CategoryStruct.comp (Y :=
    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) (Opposite.op X))))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X)) :
      Opposite.unop (Opposite.op X) ⟶
        Opposite.unop
          (Opposite.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} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
    (CategoryStruct.comp (Y :=
        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)
            (Opposite.unop
              (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.op X))))))
        (Functor.map (shiftFunctor C m)
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)))) :
          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) (Opposite.op X))) ⟶
            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)
                (Opposite.unop
                  (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.op X))))))
        (Functor.map (shiftFunctor C n ⋙ shiftFunctor C m)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ m n (m + n) sorry)) (Opposite.op X))) ≫
            Functor.map (shiftFunctor C n ⋙ shiftFunctor C m) x.unop ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' C n m (m + n) sorry))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd' C a (m + n) a'' sorry)) Y :
          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)
                (Opposite.unop
                  (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.op X))))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') Y) :
      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) (Opposite.op X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') Y))
  (CategoryStruct.comp (Y :=
    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) (Opposite.op X))))
    (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X)) :
      Opposite.unop (Opposite.op X) ⟶
        Opposite.unop
          (Opposite.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} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
    (CategoryStruct.comp (Y :=
        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)
            (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 (-m)) X))))))
        (Functor.map (shiftFunctor C m)
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-m)) X)))) :
          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) (Opposite.op X))) ⟶
            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)
                (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 (-m)) X))))))
        (Functor.map (shiftFunctor C m)
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ m n (m + n) sorry)) (Opposite.op X)))) ≫
            Functor.map (shiftFunctor C m) (Functor.map (shiftFunctor C n) x.unop) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' C n m (m + n) sorry))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd' C a (m + n) a'' sorry)) Y :
          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)
                (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 (-m)) X))))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') Y) :
      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) (Opposite.op X))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') Y))
Tactic: simp only [assoc, Functor.map_comp, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
    ← NatTrans.naturality_assoc,
    shiftFunctorAdd'_assoc_inv_app a n m a' (m + n) a'' (by lia) (by lia) (by lia)]