obtain style

Stream: general

[Patrick Massot]

I have a style question. I see in Reid's PR: obtain ⟨c, hc₁, hc₂⟩ : ∃ c : α, a < c ∧ c < b := dense h, which is the traditional way to use obtain to make proofs more readable. Somewhat recently, Mario extend the parsing so that we can put type annotations in rcases/rintros/obtain. Should we switch to obtain ⟨c : α, hc₁ : a < c, hc₂ : c < b⟩ := dense h,? I don't have a strong opinion here. The first version is nice because the existential quantifier is explicit, the second version makes it clearer what we indeed obtain.

[Johan Commelin]

I think both are fine. Let's use seems reasonable at that point.