Stream: math-comp users

Topic: ✔ Rewrite in existential


view this post on Zulip Ricardo (Jan 23 2023 at 20:40):

Hi everyone. In my proofs I usually find myself doing something like

move=> [k H]. move: H. rewrite !inE => /andP[H1 H2].

because inE wouldn't work before binding the existential. Is there a more concise way to do the same?

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 20:50):

move => [k]. rewrite !inE.

view this post on Zulip Pierre Roux (Jan 23 2023 at 20:59):

Maybe move=> [k /[!inE]/andP[H1 H2]].

view this post on Zulip Ricardo (Jan 24 2023 at 03:00):

Wow! They work and are a lot more concise! Thank you @Paolo Giarrusso and @Pierre Roux :smile:

view this post on Zulip Notification Bot (Jan 24 2023 at 03:00):

Ricardo has marked this topic as resolved.


Last updated: Jul 15 2024 at 21:02 UTC