Zulip Chat Archive

Stream: new members

Topic: Splitting multiple conjunctions in one go


view this post on Zulip 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)

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2020 at 15:43):

Yep, rcases:

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

view this post on Zulip Donald Sebastian Leung (Mar 02 2020 at 02:07):

Thanks, that made my proof script much cleaner


Last updated: May 14 2021 at 04:22 UTC