Zulip Chat Archive

Stream: new members

Topic: Intros then subst


view this post on Zulip Patrick Stevens (Jul 02 2020 at 21:22):

Is there a tactic that does "intros and then immediately subst", suitable for things like proving e.g. $x \ne 0$?

view this post on Zulip Patrick Stevens (Jul 02 2020 at 21:23):

By analogy with rcases I tried intros rfl but that just made a variable called rfl

view this post on Zulip Reid Barton (Jul 02 2020 at 21:23):

rintros rfl

view this post on Zulip Patrick Stevens (Jul 02 2020 at 21:24):

… clearly I did not take the analogy far enough, thanks


Last updated: May 11 2021 at 21:10 UTC