e82cd9b62c
This PR refines how the `apply` tactic (and related tactics like `rewrite`) name and tag the remaining subgoals. Assigned metavariables are now filtered out *before* computing subgoal tags. As a consequence, when only one unassigned subgoal remains, it inherits the tag of the input goal instead of being given a fresh suffixed tag. User-visible effect: proof states that previously displayed tags like `case h`, `case a`, or `case upper.h` for a single remaining goal now display the input goal's tag directly (e.g. no tag at all, or `case upper`). This removes noise from `funext`, `rfl`-style, and `induction`-alternative goals when the applied lemma introduces only one non-assigned metavariable. Multi-goal applications are unaffected — their subgoals continue to receive distinguishing suffixes. This may affect users whose proofs rely on the previous tag names (for example, `case h => ...` after `funext`). Such scripts need to be updated to use the input goal's tag instead. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
23 lines
1 KiB
Text
23 lines
1 KiB
Text
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 3, "character": 2}}
|
|
{"rendered": "```lean\ncase right\n⊢ True\n```",
|
|
"goals": ["case right\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 9, "character": 2}}
|
|
{"rendered": "```lean\n⊢ True ∧ True\n```", "goals": ["⊢ True ∧ True"]}
|
|
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 13, "character": 2}}
|
|
{"rendered": "```lean\ncase right\n⊢ True\n```",
|
|
"goals": ["case right\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 20, "character": 2}}
|
|
{"rendered": "```lean\ncase right\n⊢ True\n```",
|
|
"goals": ["case right\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 26, "character": 2}}
|
|
{"rendered": "```lean\ncase right\n⊢ True\n```",
|
|
"goals": ["case right\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///6594.lean"},
|
|
"position": {"line": 33, "character": 2}}
|
|
{"rendered": "```lean\ncase right\n⊢ True\n```",
|
|
"goals": ["case right\n⊢ True"]}
|