or.elim_left/right

Stream: Is there code for X?

[Johan Commelin]

Do we have these? I think the dot.notation would be helpful!

lemma or.elim_right {P Q : Prop} (h : P ∨ Q) (hnP : ¬ P) : Q :=
or_iff_not_imp_left.1 h hnP

lemma or.elim_left {P Q : Prop} (h : P ∨ Q) (hnQ : ¬ Q) : P :=
h.symm.elim_right hnQ

[Eric Wieser]

docs#or.resolve_left?

[Johan Commelin]

Cool! I knew they had to be somewhere.

[Michael Stoll]

I find myself using docs#or.resolve_left and docs#or.resolve_right all the time :smile:

[Kevin Buzzard]

That's because you've really got into golfy code, judging by your recent messages! ("I'm not happy with this four line proof, it's too long/ugly")

[Kevin Buzzard]

Twice recently I've tried to answer questions you've asked here and come up with new arguments which were much longer :-)

[Michael Stoll]

I'm trying to get competitive with @Junyan Xu :smile:

[Eric Rodriguez]

I find that these are really underused, and instead often we do cases on P \or Q and prove that one of the cases is contradictory, which although obviously valid feels... wrong, somehow

[Floris van Doorn]

I try to prove everything by rewriting nowadays, so if I'm in the middle of a simp_rw sequence, I just add simp_rw [hnP, false_or] at h. Of course, sometimes you're in term mode, and then resolve_left and resolve_right can be nice.