refine_struct: case tags not working?

[bryangingechen]

MWE:

import tactic

structure blah : Type :=
(f1 : ℕ)
(f2 : ℕ)

example : blah :=
begin
  refine_struct {..},
  case f1 {},
  /-
Invalid `case`: there is no goal tagged with suffix [f1].
state:
2 goals
case blah, f1
⊢ ℕ

case blah, f2
⊢ ℕ
-/
end

Also, the case tags don't show up in the widget view of the tactic state in VS Code (they still show up if I switch to the plain text view).

[bryangingechen]

@cipher1024 notes on Zulip that field f1 works instead.

Leaving this open for now since the tactic doc entry doesn't mention this (and the (text mode) tactic state says case), so there's still some potential for confusion here.

[cipher1024]

field indeed lacks documentation: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean#L437