doc: describe all simp configuration options

[kmill]

Co-authored by Marc Huisinga, with input from Leo.

[digama0]

It will probably be a lot more work than what you have already done here (thank you all for this BTW!), but it would also be useful to have examples where a user might plausibly want to turn on each option and demonstrate the difference, because the specification of the flags can be somewhat opaque if you don't know simp / type theory internals.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3870 has successfully built against this PR. (2024-04-10 14:37:52) View Log
• ✅ Mathlib branch lean-pr-testing-3870 has successfully built against this PR. (2024-04-10 15:22:44) View Log
• ✅ Mathlib branch lean-pr-testing-3870 has successfully built against this PR. (2024-04-11 13:32:30) View Log

[kmill]

@digama0 Thanks for taking a look. Regarding giving examples, I agree that they should appear somewhere. At the least, we can finally port that mathlib simp document now that we know what the simp options are, but I think eventually the plan is to have this be part of the Lean reference documentation.

[david-christiansen]

Yes, the examples definitely needs to be in the new reference! In the meantime, I think it's useful to have them here "below the fold", but it's OK not to as well.

[david-christiansen]

This is a very nicely written set of docs!