feat(category_theory/monoidal/discrete): simps (#14259)
This is a minuscule change, but it appears to work both on `master` and in the [shift functor refactor](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/trouble.20in.20.60shift_functor.60.20land) I'm aspiring towards, so I'm shipping it off for CI.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
