can't see goal state after case tactic

[fpvandoorn]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In the following example, if you put your cursor on the empty line, indented two spaces (i.e. where the next tactic should be), the goal state shows no goals (i.e. the goal state of finished case zero).
It should show the goal state of the remaining goal(s).

example (n : Nat) : n = n := by
  induction n
  case zero => rfl
  
--^

(note: the same occurs when there is a multi-line tactic block after case zero).

Context

Zulip thread

Versions

Lean 4.2.0

Impact

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

[nomeata]

I also stumbled over this, version 4.6.0-rc1; here is my duplicate issue description (with additional info about de-indenting and other tactics)

---

Consider

example (n : Nat) : n = n := by
  induction n
  case zero => rfl
  ‸

The natural thing to do next is to move the cursor to the next line, aligned with the case, as shown. But then the proof state is

Tactic state
No goals

If I de-indent once more, to

example (n : Nat) : n = n := by
  induction n
  case zero => rfl
 ‸

I see what I want to see: The list of still open goals

Tactic state
1 goal
n✝: Nat
n_ih✝: n✝ = n✝
⊢ Nat.succ n✝ = Nat.succ n✝

But de-indenting further left seems wrong here.

It does not happen with · nor next; there we get the desired behavior.

Maybe the parser for case can be adjusted accordingly.

Odd, the parsers for next and case look very similar:

syntax (name := case) "case " sepBy1(caseArg, " | ") " => " tacticSeq : tactic

macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)

So not sure why it works for some and not the others.

[Seasawher]

suffices ... by notation has same issue. (Lean version: v4.8.0-rc1)

example {a b : Nat} (h : a = b) : b ≤ b + 1 := by
  suffices a ≤ a + 1 by
    /-
    a b : Nat
    h : a = b
    ⊢ a ≤ a + 1
    -/
    sorry

  suffices a ≤ a + 1 from by
    /-
    a b : Nat
    h : a = b
    this : a ≤ a + 1
    ⊢ a ≤ a + 1
    -/
    sorry

  simp [h]