exists.elim multiple

Stream: new members

[Bjørn Kjos-Hanssen]

have h: ∃ x y z : ℕ, x+y=z,
exists.elim h ( ...)

Is there a way to discharge all the variables x y z at once instead of using three nested exists.elim's?

[Patrick Johnson]

In tactic mode you can use docs#tactic.rcases

rcases h with ⟨x, y, z, h⟩