# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Destruct multiple disjunctions

#### Adam Topaz (Oct 08 2020 at 15:49):

Suppose I have a number of disjunctions (or some other inductive type) are hypotheses in my context. Is there a tactic that will case split on all of them and give the appropriate number of subgoals? Is there some `rcases`

magic that will do this?

Here is a silly example:

```
import tactic
variables (p1 p2 q1 q2 c11 c12 c21 c22 : Prop)
(h11 : p1 ∧ q1 → c11)
(h12 : p1 ∧ q2 → c12)
(h21 : p2 ∧ q1 → c21)
(h22 : p2 ∧ q2 → c22)
include h11 h12 h21 h22
example : p1 ∨ p2 → q1 ∨ q2 → c11 ∨ c12 ∨ c21 ∨ c22 :=
begin
intros h1 h2,
cases h1,
{ cases h2,
{ left, finish [h11] },
{ right, left, finish [h12] }},
{ cases h2,
{ right, right, left, finish [h21] },
{ right, right, right, finish [h22] }},
end
```

I would be much happier if I didn't have to write `cases h2`

twice.

#### Adam Topaz (Oct 08 2020 at 15:52):

It would be nice if, in this case, I could write something along the lines of

```
rcases [h1,h2] with [h1|h1,h2|h2],
```

#### Shing Tak Lam (Oct 08 2020 at 16:01):

```
example : p1 ∨ p2 → q1 ∨ q2 → c11 ∨ c12 ∨ c21 ∨ c22 :=
begin
rintros (h1 | h1) (h2 | h2),
-- 4 goals here
all_goals {finish}
end
```

#### Adam Topaz (Oct 08 2020 at 16:01):

okay, sure that works for this example. But my actual assumptions are a bit more complicated than this.

#### Reid Barton (Oct 08 2020 at 16:02):

`rcases h1 with h1 | h1; rcases h2 with h2 | h2,`

#### Adam Topaz (Oct 08 2020 at 16:03):

Yeah that's exactly what I'm looking for. Didn't think of using `;`

thanks!

#### Floris van Doorn (Oct 08 2020 at 21:40):

Another way to do this:

```
obtain ⟨hp1|hp2, hq1|hq12⟩ : _ ∧ _ := ⟨h1, h2⟩,
```

#### Adam Topaz (Oct 08 2020 at 21:43):

That's a nice trick!

#### Mario Carneiro (Oct 11 2020 at 07:15):

This is now supported as of #4569:

```
example : p1 ∨ p2 → q1 ∨ q2 → c11 ∨ c12 ∨ c21 ∨ c22 :=
begin
intros h1 h2,
rcases ⟨e1, e2⟩ with ⟨h1 | h1, h2 | h2⟩,
end
```

```
example : p1 ∨ p2 → q1 ∨ q2 → c11 ∨ c12 ∨ c21 ∨ c22 :=
begin
intros h1 h2,
obtain ⟨h1 | h1, h2 | h2⟩ := ⟨e1, e2⟩,
end
```

in addition to the already supported `rintros (h1 | h1) (h2 | h2),`

form that was mentioned

Last updated: May 07 2021 at 21:10 UTC