# Zulip Chat Archive

## Stream: new members

### Topic: Reducing cases

#### Chris M (Jun 15 2020 at 04:24):

I have come across a situation where a proposition `X`

implies a disjunctive `A\or B\or C`

. A, B, C are cases, but I can reduce case C to case B, i.e. `lemma2: C\to B`

holds. I *could* write this as follows:

```
assume hX:X,
have h2: (A \or B) \or C, from lemma1 hX,
have h3: A \or B from or.elim h2 (assume h4:A \or B, h4) (assume h5:C, or.intro A (lemma2 h5))
```

However, this seems unnecessarily messy, and it seems I should be able to just "reduce C to B" in approximately one command, rather than having to consider the `A`

and `B`

cases as well. Is this possible?

#### Chris Wong (Jun 15 2020 at 05:08):

If you group the B and C together with `or.assoc`

, then you can use `or.imp_right`

to map that to `B \or B`

then collapse it with `or_self`

#### Chris Wong (Jun 15 2020 at 05:08):

I think in general though we tend to use tactics like `cc`

, which lessen the need to make manual manipulation easy

#### Mario Carneiro (Jun 15 2020 at 05:10):

There should be a theorem that says `(q -> p) -> (p \/ q <-> p)`

that should be usable here

#### Mario Carneiro (Jun 15 2020 at 05:16):

```
example (a b c : Prop) (h : a ∨ b ∨ c) (h2 : c → b) : false :=
begin
have := h.imp_right (or_iff_left_of_imp h2).1,
end
```

The advantage of this over using `cc`

is that you don't have to assert the goal statement, it is a purely syntactic transformation so `a,b,c`

can be any expressions and they will not be unduly affected by the tactic

#### Mario Carneiro (Jun 15 2020 at 05:18):

The fancy tactic version is

```
example (a b c : Prop) (h : a ∨ b ∨ c) (h2 : c → b) : false :=
begin
have : a ∨ b := by tauto!,
end
```

#### Mario Carneiro (Jun 15 2020 at 05:23):

the other advantage of the first method is that the type of `h2`

is already determined by the context here so you can even do this in a way where `h2`

is a subgoal rather than a hypothesis:

```
example (a b c : Prop) (h : a ∨ b ∨ c) : false :=
begin
have := h.imp_right (or_iff_left_of_imp (λ hb, _)).1,
{ -- this: a ∨ b |- false
sorry },
{ -- hb: b |- c
sorry },
end
```

Last updated: May 10 2021 at 00:31 UTC