refine_struct cases

Stream: general

[Yury G. Kudryashov]

I called refine_struct { .. } on an equiv goal, and it generated 4 goals, first of them labeled case equiv, to_fun.

[Yury G. Kudryashov]

How do I focus those goals by name?

[Yury G. Kudryashov]

I tried case equiv to_fun, case equiv.to_fun, case "equiv, to_fun"

[Johan Commelin]

@Simon Hudon :up:

[Mario Carneiro]

You can't, at least not with case

[Mario Carneiro]

case is explicitly filtering for cases that are tagged with _case or _case_simple, while refine_struct generates cases tagged with _field

[Mario Carneiro]

I hadn't realized that there is an additional hidden tag marker like this. This seems like a dubious feature, since there is no UI indication that this case is any different from the kind of case you get from the inductive tactic

[Kevin Buzzard]

Ooh tag markers. That's new

[Simon Hudon]

with refine_struct, you use field instead of case. You use it as field my_struct_field { tactic }

[Simon Hudon]

You can use have_field to stand for have field := @my_struct.some_field