feat: grind tests for basic category theory

[kim-em]

This PR adds additional tests for grind, demonstrating that we can automate some manual proofs from Mathlib's basic category theory library, with less reliance on Mathlib's @[reassoc] trick.

In several places I've added bidirectional patterns for equational lemmas.

I've updated some other files to use the new @[grind_eq] attribute (but left as is all cases where we are inspecting the info messages from grind_pattern).

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 76f883b9995f684663e3106b08defec46f7a7f4c --onto dc5c8097b5ca053dd49b5de246add54c3e999734. (2025-01-06 00:50:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2ed77f3b262bb2b2c509e95ac01e6fe161ed40fd --onto dc5c8097b5ca053dd49b5de246add54c3e999734. (2025-01-06 06:52:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2c9641f621f8aecf69d8644d5b7f99c96cb947fa --onto 78ddee911287bf7b0069a695b01001db2654a765. (2025-01-06 16:31:33)