refine tactic syntax for inductive types

Stream: lean4

[Yakov Pechersky]

What's the right incantation to make the following work?

example (hp : p) (hq : q) : And p q := by
  refine ⟨_, _⟩; -- errors here, does not produce two goals
  exact hp; -- says "no goals to be solved" here
  exact hq

[Mario Carneiro]

example (hp : p) (hq : q) : And p q := by
  refine ⟨?_, ?_⟩;
  exact hp;
  exact hq

[Yakov Pechersky]

Thanks Mario. I see that produces two cases refine_1 and refine_2. Is there a way to name them?

[Mario Carneiro]

example (hp : p) (hq : q) : And p q := by
  refine ⟨?a, ?b⟩
  case a => exact hp
  case b => exact hq

[Yakov Pechersky]

Sweet, thanks

[Yakov Pechersky]

By the way, when did we get Go-To-Defn working in VSCode?! It's awesome!

[Yakov Pechersky]

And the infoview working...