using cases more efficiently

Stream: new members

[Heather Macbeth]

Here are two manipulations that took me two lines each, using intros and cases. They seem like very standard combinations, so I would like to know if there are tactics that would do them in one line? For the first, the answer is probably rcases, but I couldn't figure out the syntax.

variables {E : Type}

example (P : E → Prop) (s : set E) (Q : Prop) (h : ∃ x ∈ s, P x) : Q :=
begin
  cases h with x h',
  cases h' with H hP,
  sorry,
end

example (P : E × E → Prop) : ∀ x : E × E, P x :=
begin
  intros x,
  cases x with a b,
  sorry,
end

[Yakov Pechersky]

rcases and rintros

[Yakov Pechersky]

variables {E : Type}

example (P : E → Prop) (s : set E) (Q : Prop) (h : ∃ x ∈ s, P x) : Q :=
begin
  rcases h with ⟨x, H, hP⟩,
  sorry,
end

example (P : E × E → Prop) : ∀ x : E × E, P x :=
begin
  rintros ⟨a, b⟩,
  sorry,
end

[Jalex Stark]

those are \lan and \ran, in case the notation is unfamiliar

[Heather Macbeth]

Great :grinning:

[Yakov Pechersky]

I use \< and \>, which also work

[Bryan Gin-ge Chen]

For extra efficiency, you can even type \<>+tab and VS Code will put your cursor in between the brackets.