Zulip Chat Archive

Stream: new members

Topic: Splitting multiple conjunctions in one go

Donald Sebastian Leung (Mar 01 2020 at 15:38):

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 (Mar 01 2020 at 15:43):

Yep, rcases:

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

Donald Sebastian Leung (Mar 02 2020 at 02:07):

Thanks, that made my proof script much cleaner

Last updated: Dec 20 2023 at 11:08 UTC