nested cases

Stream: general

[Reid Barton]

Is there a more convenient way to unpack the components of a conclusion of the form ∃ x y, p x ∧ q y ∧ r x y in a tactics block than using multiple cases tactics?

[Andrew Ashworth]

you want mathlib's rcases or core's cases_matching

[Reid Barton]

oh yeah, rcases is what I want. Much better!

[Sean Leather]

@Reid Barton Also, in case you didn't know, the anonymous constructor notation ⟨..., ...⟩ is right-associative for nested constructors. So, for example, you can do rcases h with ⟨x, y, px, qy, rxy⟩ with your type. I learned this recently, and it's quite convenient.