obtain rfl

Stream: general

[Johan Commelin]

I just noticed that we can now replace the pattern

have : x = 0 := foobar baz xyzzy,
subst x -- or `subst this`

with

obtain rfl : x = 0 := foobar baz xyzzy

[Floris van Doorn]

Yeah, the obtain tactic very nice!

[Rob Lewis]

Note that if foobar baz xyzzy elaborates without the expected type, this is really just cases foobar baz xyzzy. And even if you use obtain, the rfl shouldn't be necessary.