## 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: May 11 2021 at 21:10 UTC