Zulip Chat Archive

Stream: new members

Topic: using cases more efficiently


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 02:18):

rcases and rintros

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 18 2020 at 02:19):

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

view this post on Zulip Heather Macbeth (Jun 18 2020 at 02:19):

Great :grinning:

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 02:20):

I use \< and \>, which also work

view this post on Zulip 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