decompose conjuction/existence chain

Stream: Is there code for X?

[Jelmer Firet]

Suppose H is an hypothesis with conjuctions and existentials;
for example H = a /\ b /\ exists x, c
Is there a tactic that splits this into all it's parts, something like this:

H : A ∧ B ∧ ∃ x : ℕ, C
======================
Goal

decompose H with a b x c,

a : A
b : B
x : ℕ
c : C x
=======
Goal

Instead of having to write

cases H with a H,
cases H with b H,
cases H with x c,

[Eric Wieser]

tactic#rcases and tactic#obtain both do that

[Eric Wieser]

obtain ⟨a, b, x, c⟩ := H

[Jelmer Firet]

I will check those out, thanks!