double cases

Stream: general

[orlando]

Hello, a Little question :

i have a property truc : ∃ (s : S ) (u : U), blabla it's possible obtain directly s, u, hyp_blabla
for the moment i do 2 line :

cases truc with s h_s,
cases h_s with u hyp_blabla,

I'm sure this is possible but i don't remember :confused:

[Kevin Buzzard]

rcases truc with \<s, u, hyp\>

[orlando]

ohhh my bad : i use rcases truc with ⟨s, u hyp⟩, i forget the , stupid me !!!

Thx Kevin !

[Kevin Buzzard]

I watched 20 undergraduates playing a preliminary version of the natural number game last year and they always forgot the comma :-)