## 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