-- 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
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ Eq (α := ShiftedHom X Z c)
    ((Equiv.symm (opEquiv c) : (a : ShiftedHom (Opposite.op Z) (Opposite.op X) c) → ShiftedHom X Z c) (f.comp g h) :
      ShiftedHom X Z c)
    (comp (Y := Y) ((Equiv.symm (opEquiv b) : (a : ShiftedHom (Opposite.op Y) (Opposite.op X) b) → ShiftedHom X Y b) g)
        ((Equiv.symm (opEquiv a) : (a_1 : ShiftedHom (Opposite.op Z) (Opposite.op Y) a) → ShiftedHom Y Z a) f) ⋯ :
      ShiftedHom X Z c)
have rw : Eq (α := ShiftedHom X Z c)
  (Quiver.Hom.unop
      (CategoryStruct.comp (Y :=
        Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c)
            (Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a) (Opposite.op X)))))
        (Quiver.Hom.op
          (Functor.map (shiftFunctor C c)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ b a c sorry)) (Opposite.op X)))))
        (Quiver.Hom.op
            (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c sorry))
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a) (Opposite.op X)))) ≫
          CategoryStruct.comp (Y :=
            Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (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ᵒᵖ b) (Opposite.op X))))))
            (Quiver.Hom.op
                (Functor.map (shiftFunctor C b)
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a)))
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))) :
              Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                    (Opposite.unop
                      (Functor.obj.{v_1, v_1, u_1, u_1}
                        (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙
                          Equivalence.inverse (opShiftFunctorEquivalence C a))
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b) (Opposite.op X))))) ⟶
                Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                    (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ᵒᵖ b) (Opposite.op X))))))
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X) :
              Functor.obj.{v_1, v_1, u_1, u_1}
                  (Equivalence.functor (opShiftFunctorEquivalence C b) ⋙
                    Equivalence.inverse (opShiftFunctorEquivalence C b))
                  (Opposite.op X) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)))) ≫
    Functor.map (shiftFunctor C c)
      (f ≫
          Functor.map (shiftFunctor Cᵒᵖ a) g ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' Cᵒᵖ b a c h)) (Opposite.op X)).unop)
  (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C b) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C b))
            (Opposite.op X)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C b))) (Opposite.op X)))
        (Functor.map (shiftFunctor C b) (Quiver.Hom.unop g)) :
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Opposite.unop (Opposite.op Y)))
    (Functor.map (shiftFunctor C b)
          ((Equiv.symm (opEquiv a) : (a_1 : ShiftedHom (Opposite.op Z) (Opposite.op Y) a) → ShiftedHom Y Z a) f) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c sorry)) Z :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) Z))
Tactic: rw [opEquiv_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (show a + b = c by lia), comp, comp]