Splitting product-like hypotheses

Stream: Is there code for X?

[Jannis Limperg]

Is there a tactic for splitting all product-like hypotheses? E.g. for the goal

A B X : Type,
P Q : Prop,
R : X → Prop,
h : P ∧ Q,
i : ∃ (x : X), R x,
j : A × B
⊢ false

the tactic would produce

A B X : Type,
P Q : Prop,
R : X → Prop,
h_1 : P
h_2 : Q
i_1 : X
i_2 : R i_1
j_1 : A
j_2 : B

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib_docs/tactics.html#cases_matching%20/%20casesm or the next one maybe

[Jannis Limperg]

Thanks! This doesn't do exactly what I want (I'd like to split things like ∀ x, P x ∧ Q x as well), so I'll probably have to implement it myself.