Splitting multiple conjunctions in one go

Stream: new members

[Donald Sebastian Leung]

Suppose I have a hypothesis of the form h : P₁ ∧ P₂ ∧ ... ∧ Pn. Currently, I find myself doing:

cases h with hP₁ h,
cases h with hP₂ h,
...
cases h with hPn_1 hPn,

which is rather tedious. Is there a way to split all those conjunctions in one go? (Same for hypotheses of the form ∃ x₁ x₂ ... xn, P)

[Bryan Gin-ge Chen]

Yep, rcases:

rcases h with ⟨hP_1, hP_2, ..., hPn⟩

[Donald Sebastian Leung]

Thanks, that made my proof script much cleaner