ComposableArrows incompatible with simproc Fin.reduceFinMk. #27382
Description
The simproc Fin.reduceFinMk causes breakages in Mathlib/CategoryTheory/ComposableArrows.lean: in particular CategoryTheory.ComposableArrows.Precomp.obj_succ seems strongly affected. (e.g. dsimp can now simplify 2 + 3 to 5). For now, we just turn off the offending simprocs in this file and write simp [-Fin.reduceFinMk] whenever Precomp.obj_succ is required.
However, hopefully it is possible to refactor the material here so that no disabling of simprocs is needed.
This issue existed since the introduction of the Fin.reduceFinMk simproc, but we decided to track it since #27351, where it became much clearer what exactly is to blame.