feat: FunInd: more equalities in context, more careful cleanup

[nomeata]

A round of clean-up for the context of the functional induction principle cases.

• Already previously, with match e with | p => …, functional induction would ensure that h : e = p is in scope, but it wouldn’t work in dependent cases. Now it introduces heterogeneous equality where needed (fixes FunInd chokes on pattern match with dependent targets #4146)
• These equalities are now added always (previously we omitted them when the discriminant was a variable that occurred in the goal, on the grounds that the goal gets refined through the match, but it’s more consistent to introduce the equality in any case)
• We no longer use MVarId.cleanup to clean up the goal; it was sometimes too aggressive (fixes incorrect functional induction principle #5347)
• Instead, we clean up more carefully and with a custom strategy:
  • First, we substitute all variables without a user-accessible name, if we can.
  • Then, we substitute all variable, if we can, outside in.
  • As we do that, we look for HEqs that we can turn into Eqs to substitute some more
  • We substitute unused lets.

Breaking change: In some cases leads to a different functional induction principle (different names and order of assumptions, for example).

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-09-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-09-16 10:33:27)
• ✅ Mathlib branch lean-pr-testing-5364 has successfully built against this PR. (2024-09-16 11:43:26) View Log