rcases leaking subgoals out of have

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Using rcases on a term containing a hole leads to subgoals leaking out of the current have.

Context

This was discussed on Zulip. I came across this while refactoring something in the sphere eversion project.

Steps to Reproduce

My original minimization was:

example : True := by
  have : ∃ k, 5 = 2 + k := by
    -- Using apply with a hole create a new goal right here
    -- apply Nat.exists_eq_add_of_le (?_ : 2 ≤ 5)
    -- Using rcases teleports the new goal outside of the have block
    rcases Nat.exists_eq_add_of_le (?_ : 2 ≤ 5) with ⟨k, hk⟩
    exact ⟨k, hk⟩
  trivial -- This trivial solves 2 ≤ 5
  trivial -- this one takes care of True

Kyle came up with a variant where the hole is not directly inside rcases but in a let:

example : True := by
  have : ∃ k, 5 = 2 + k :=
    let h := Nat.exists_eq_add_of_le (?_ : 2 ≤ 5)
    by
      rcases h with ⟨k, hk⟩
      exact ⟨k, hk⟩
  trivial -- this one takes care of True
  trivial -- This trivial solves 2 ≤ 5

Expected behavior: [Clear and concise description of what you expect to happen]

The new subgoal should be inside the have.

Actual behavior: [Clear and concise description of what actually happens]

The new subgoal leaks outside the have.

Versions

Found with 4.8.0, reproduced in 4.9.0-nightly-2024-06-02 on live.lean-lang.org.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the two minimal Lean examples in the issue and reproduce the behavior against the reported nightly version. Compare the direct rcases case with the let variant and the commented apply form. Done means subgoals created by the hole remain inside the have block in both examples.