fix: WF.Fix: deduplicate subsumed goals before running tactic

[nomeata]

before code like

def dup (a : Nat) (b : Nat := a) := a + b

def rec : Nat → Nat
 | 0 => 1
 | n+1 => dup (dup (dup (rec n)))
decreasing_by decreasing_tactic

would run the decreasing_tactic 8 tims, because the recursive call
rec n gets duplicate due to the default paramter. Similar effects can
be observed due to dependent types or tactics like cases.

This is wasteful, and is confusing to the user when they use
decreasing_by interactively. Therfore, we now go through the proof
obligations (MVars) and if solving one would imply solving another one,
we assign the mvars to each other accordingly.

This PR is a sibling of #3004.

[nomeata]

I’ll run this against mathlib once 9290b49 is tagged as nightly-with-mathlib.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-05' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-05 09:34:51)
• ✅ Mathlib branch lean-pr-testing-3024 has successfully built against this PR. (2023-12-05 13:51:32) View Log
• ✅ Mathlib branch lean-pr-testing-3024 has successfully built against this PR. (2023-12-05 15:18:23) View Log
• ✅ Mathlib branch lean-pr-testing-3024 has successfully built against this PR. (2023-12-06 10:05:23) View Log
• ✅ Mathlib branch lean-pr-testing-3024 has successfully built against this PR. (2023-12-06 16:29:01) View Log
• ✅ Mathlib branch lean-pr-testing-3024 has successfully built against this PR. (2023-12-06 18:15:57) View Log

[nomeata]

Got mathlib perf results, nothing to see. http://speed.lean-fro.org/mathlib4/compare/6d60f603-6faa-4727-9a04-42abb15e1477/to/535315ad-b4ab-4d6a-b3fd-67e8b2ff12c7

There is an “open Mathlib — wall-clock 7.8%” but I think it’s a fluke: It doesn't show up when comparing this branch with the latest master, and it it seems unlikely that there is a change in testing-nightly that improved open Mathlib by exactly the amount that this regressed then. Also “open Mathlib – instructions” goes down.