## Stream: new members

### Topic: using cases more efficiently

#### Heather Macbeth (Jun 18 2020 at 02:16):

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 (Jun 18 2020 at 02:18):

rcases and rintros

#### Yakov Pechersky (Jun 18 2020 at 02:18):

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 (Jun 18 2020 at 02:19):

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

Great :grinning:

#### Yakov Pechersky (Jun 18 2020 at 02:20):

I use \< and \>, which also work

#### Bryan Gin-ge Chen (Jun 18 2020 at 02:25):

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

Last updated: May 14 2021 at 06:16 UTC