Zulip Chat Archive
Stream: new members
Topic: Intros then subst
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$?
Patrick Stevens (Jul 02 2020 at 21:23):
By analogy with rcases I tried intros rfl but that just made a variable called rfl
Reid Barton (Jul 02 2020 at 21:23):
rintros rfl
Patrick Stevens (Jul 02 2020 at 21:24):
… clearly I did not take the analogy far enough, thanks
Last updated: Dec 20 2023 at 11:08 UTC