fix: check that funind-reserved names are available

[nomeata]

I did not introduce inductTheoremSuffix etc, it seems more direct to just spell out the suffix here. If we ever change it there are many occurrences where they need to be changed anyways, so the definition doesn't seem to save much work or add that much robustness.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4135 has successfully built against this PR. (2024-05-11 12:55:17) View Log
• ✅ Mathlib branch lean-pr-testing-4135 has successfully built against this PR. (2024-05-11 13:36:59) View Log
• ✅ Mathlib branch lean-pr-testing-4135 has successfully built against this PR. (2024-05-11 15:38:57) View Log