five goals in infoview after cases

Stream: lean4

[Kevin Buzzard]

import Mathlib.Data.Equiv.Basic

def to : Bool × α → α ⊕ α
| (true, a) => Sum.inl a
| (false, a) => Sum.inr a

def inv : α ⊕ α → Bool × α
| Sum.inl a => (true, a)
| Sum.inr a => (false, a)

def equ : Equiv (Bool × α) (α ⊕ α) :=
{ toFun := to
  invFun := inv
  left_inv := λ x =>
  match x with
  | (true, _) => rfl
  | (false, _) => rfl
  right_inv := λ b => by
    cases b
    rfl --why does tactic state display 5 goals if cursor is here?
    rfl
}

Why do I get 5 goals displayed after the last-but-one rfl? The proof is fine.

[Henrik Böving]

If you use the trace_state tactic you can see there is only one goal really around here in its output. As to why the goal view is doing this I don't really know but given the fact that you are probably using VSCode and I am using Emacs it's most likely an issue with the language server in the Lean compiler (although merely a cosmetic one of course)