feat: where ... finally section to assign leftover goals

[sgraf812]

This PR implements a finally section following a (potentially empty) where block. where ... finally opens a tactic sequence block in which the goals are the unassigned metavariables from the definition body and its auxiliary definitions that arise from use of let rec and where.

This can be useful for discharging multiple proof obligations in the definition body by a single invocation of a tactic such as all_goals:

example (i j : Nat) (xs : Array Nat) (hi : i < xs.size) (hj: j < xs.size) :=
  match i with
  | 0 => x
  | _ => xs[i]'?_ + xs[j]'?_
where x := 13
finally all_goals assumption

[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 2629921c0173f6bb8dccc9f0b74433c362b4d009 --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 14:54:05)
• ✅ Mathlib branch lean-pr-testing-8723 has successfully built against this PR. (2025-06-12 16:30:45) View Log
• ✅ Mathlib branch lean-pr-testing-8723 has successfully built against this PR. (2025-06-20 16:53:19) View Log