-- 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 Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            (Opposite.op X)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)))
        (Functor.map (shiftFunctor C n)
          (Quiver.Hom.unop
            (Quiver.Hom.op g ≫
              CategoryStruct.comp (Y :=
                Functor.obj.{v_1, v_1, u_1, u_1}
                  (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                    Equivalence.functor (opShiftFunctorEquivalence C n))
                  (Opposite.op Y))
                (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y))
                (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f))))) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z =
    f.comp g ⋯
have dsimp : 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 X))))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
        Opposite.unop (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 X))))))
      (Functor.map (shiftFunctor C n)
          (CategoryStruct.comp (Y :=
              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) Y))))
              (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f)) :
                Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op 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) Y))))
              (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y)) :
                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) Y))) ⟶
                  Opposite.unop (Opposite.op Y)) ≫
            g) :
        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 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) Z)) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q sorry)) Z =
  f ≫ Functor.map (shiftFunctor C n) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q sorry)) Z
Tactic: dsimp [comp]