Instance hell when implementing PROPs

Stream: general

[finegeometer]

I was trying to implement PROPs, a particular kind of monoidal category, and morphisms between them. This is what I have so far.

import Mathlib.CategoryTheory.Bicategory.SingleObj
import Mathlib.CategoryTheory.Bicategory.Strict
import Mathlib.CategoryTheory.Monoidal.Braided.Basic

-- https://ncatlab.org/nlab/show/PROP
structure PROP where
  cat : @CategoryTheory.Category ℕ
  mon : @CategoryTheory.MonoidalCategory ℕ cat
  symm : @CategoryTheory.SymmetricCategory ℕ cat mon
  strict : CategoryTheory.Bicategory.Strict (@CategoryTheory.MonoidalSingleObj ℕ cat mon)
  tensorObj_is_add : mon.tensorObj = Nat.add

structure PROP.Hom (P1 P2 : PROP) where
  functor : @CategoryTheory.BraidedFunctor
    ℕ P1.cat P1.mon
    (@CategoryTheory.SymmetricCategory.toBraidedCategory ℕ P1.cat P1.mon P1.symm)
    ℕ P2.cat P2.mon
    (@CategoryTheory.SymmetricCategory.toBraidedCategory ℕ P2.cat P2.mon P2.symm)
  functor_preserves_objects :
    (@Prefunctor.obj ℕ P1.cat.toQuiver ℕ P2.cat.toQuiver
      $ @CategoryTheory.Functor.toPrefunctor ℕ P1.cat ℕ P2.cat
      $ @CategoryTheory.LaxMonoidalFunctor.toFunctor ℕ P1.cat P1.mon ℕ P2.cat P2.mon
      $ @CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor ℕ P1.cat P1.mon ℕ P2.cat P2.mon
      $ @CategoryTheory.BraidedFunctor.toMonoidalFunctor
          ℕ P1.cat P1.mon (@CategoryTheory.SymmetricCategory.toBraidedCategory ℕ P1.cat P1.mon P1.symm)
          ℕ P2.cat P2.mon (@CategoryTheory.SymmetricCategory.toBraidedCategory ℕ P2.cat P2.mon P2.symm)
      $ functor
    ) = id

That last line, functor_preserves_objects, should be as simple as functor.obj = id.
But if I write that, Lean can't figure out the correct instances.
So I'm stuck with this nine-line mess.

Is there a way to simplify this? Alternatively, is there a better design for these definitions?

[Yaël Dillies]

I have already written some code about PROPs, let me dig it up