Commit 2024-08-19 09:50 aa93a5e6
View on Github →chore(test/CategoryTheory/Elementwise): use MonCat (#15219)
This addresses a TODO from the port.
One test only works with an erw and rfl; help from an expert fixing this is welcome. Remove one set_option which did not do anything.