Commit 2025-08-05 23:45 9845f69f

feat: replace aesop_cat with a configurable discharger (#27938) This PR

• replaces aesop_cat with cat_disch
• by default, cat_disch calls the original implementation of aesop_cat
• but an option configures it to call grind instead
• and adds logging options To make further use of grind in the category theory library:

1. Turn on set_option mathlib.tactic.category.log_aesop.
2. Run lake build
3. In files that report they are using aesop as the discharger, add set_option mathlib.tactic.category.grind true (and leave this set in your PR), and fix any problems.
4. Eventually, we can consider changing over the defaults. I have a branch grind_cat which starts switching over to the grind based discharger. It can close many goals that aesop_cat can't. This looks like a huge PR, but besides the changes to Mathlib/CategoryTheory/Category/Basic.lean and Mathlib/CategoryTheory/Category/Init.lean, all other changes are search and replace by aesop_cat to by cat_disch.