open subgoal elsewhere changes refine behavior

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

Consider the following to examples:

example : True ∧ True := by
  constructor
  · sorry
  · -- fails
    refine (Decidable.byContradiction fun h => ?_ :) 
    sorry
    sorry
    
example : True ∧ True := by
  constructor
  · skip
  · -- succeeds
    refine (Decidable.byContradiction fun h => ?_ :) 
    sorry
    sorry

It is surprising that the existence of an open subgoal elsewhere changes the behavior of refine.

Context

This lead to undesired behavior in the by_contra tactic leanprover-community/batteries#1196 (which will likely be patched independent of this issue.

Versions

4.21.0-rc3

Impact

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

Start by reproducing the two minimal examples on the Lean nightly release, comparing the refine behavior when the earlier subgoal uses sorry versus skip. The issue names no source file or test path; done means the behavior no longer depends on an unrelated open subgoal and a regression test covers both examples.