rcases vs. obtain

Stream: new members

[Kenny Lau]

What is rcases doing now that we have obtain?

[Kenny Lau]

aha, rcases clears the hypothesis as well! i just bumped into a case where this was useful.

[Notification Bot]

Kenny Lau has marked this topic as resolved.

[Aaron Liu]

obtain also clears the hypothesis???

[Notification Bot]

Kenny Lau has marked this topic as unresolved.

[Kenny Lau]

oh, that's right too, lol

[Kyle Miller]

Having both lets you write in boustrophedon order so your eyes don't get as tired reading Lean code.

obtain ⟨a,b,c⟩ := x
rcases a with ⟨d,e,f⟩
obtain ⟨g,h,i⟩ := d
rcases g with ⟨j,k,l⟩

[Aaron Liu]

but which one is ltr and which one is rtl

[Kenny Lau]

the other one!

[Aaron Liu]

rcases lets you omit the pattern and obtain lets you delay the value

[Aaron Liu]

but obtain lets you omit the pattern too...

[Ruben Van de Velde]

Jokes aside, they're functionally the same

[Ruben Van de Velde]

I'd be inclined towards deprecating rcases, though I'm not sure it's worth the churn in mathlib

[Aaron Liu]

oh but when you obtain without a pattern it goes into this and when you rcases without a pattern it splits the discriminant into cases

[Ruben Van de Velde]

Also I'd prefer if we could merge obtain into have/let, but not sure if there's appetite for that

[Kevin Buzzard]

Commelin pointed out to me that obtain is a word and rcases is a mathlibism, and I've never used rcases since.

[Aaron Liu]

what does rcases even stand for? "recursive cases"?