obtain

Stream: general

[Johan Commelin]

I just realised there is obtain:
https://github.com/leanprover/mathlib/search?q=obtain&unscoped_q=obtain

[Johan Commelin]

I have not yet figured out what it does.

[Bryan Gin-ge Chen]

I think I looked it up before and I concluded it was a lean 2 thing?

[Mario Carneiro]

it is a lean 2 thing. obtain x h, from expr, expr' is the lean 2 way of writing let <x, h> := expr in expr', at least when expr has exists type. I forget how general it is

[Mario Carneiro]

the style guide also uses take, which is no longer a keyword and is the same as λ

[Johan Commelin]

Ok, thanks for explaining!

[Floris van Doorn]

obtain used to work on all inductive types with a single constructor. It was the way to do cases in term mode.

[Scott Morrison]

I just found myself writing

 obtain ⟨V, ⟨m,h₂⟩⟩ : _ := f.r U h₁

i.e. using obtain, but not wanting to specify the type. This is synonymous with

rcases f.r U h₁ with ⟨V, ⟨m,h₂⟩⟩,

but I wonder if we should just support dropping the type specification in obtain, if the proof is given after :=.

[Scott Morrison]

(Really I'd like have to just do this...)

[Rob Lewis]

Hah, I was confused about how this topic started in November, since I just added the obtain tactic last month. We should probably get rid of the Lean 2 syntax in the style guide...

[Rob Lewis]

I didn't support that syntax in obtain because it is literally just reordering arguments to rcases. But I'll grant that it reads better with obtain sometimes.

[Rob Lewis]

And it doesn't really hurt to handle it.

[Reid Barton]

I haven't had a chance to use obtain yet but I quite like the uniformity of its syntax relative to have and let. I guess let can't do this in tactic mode?

[Rob Lewis]

I think tactic mode let doesn't destruct things at all, right?

[Rob Lewis]

https://github.com/leanprover-community/mathlib/pull/1327 by the way.