rcases abuse

Stream: general

[Patrick Massot]

I think I set a new record for my uses of rcases with rcases r_in with ⟨t_α, ⟨r_α, r_α_in, h_α⟩, t_β, ⟨r_β, r_β_in, h_β⟩, h⟩,

[Simon Hudon]

Do you think you should be sent to Lean jail? I tend to prefer just a slap on the wrist but I'm open to hearing your arguments

[Patrick Massot]

Heh, it took me a while to figure out where to put bracket. This is an artistic performance.

[Patrick Massot]

Also, I blame product uniformities.