import Mathlib.Tactic.LeftRight
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Cases

Advanced proposition world.

Level 7: or_symm

Proving that (P ∨ Q) ⟹ (Q ∨ P) involves an element of danger. intro h is the obvious start. But now, even though the goal is an ∨ statement, both left and right put you in a situation with an impossible goal. Fortunately, after intro h you can do cases h with. Then something new happens: because there are two ways to prove P ∨ Q (namely, proving P or proving Q), the cases tactic turns one goal into two, one for each case. Each branch is easy to solve using the left and right tactics we used in Level 6.

Lemma

If P and Q are true/false statements, then P ∨ Q ⟹ Q ∨ P.

lemma 
or_symm: ∀ (P Q : Prop), P ∨ Q → Q ∨ P
or_symm (
P: Prop
P 
Q: Prop
Q : 
Prop: Type
Prop) : 
P: Prop
P ∨ 
Q: Prop
Q → 
Q: Prop
Q ∨ 
P: Prop
P := by
P, Q: Prop
P ∨ Q → Q ∨ P
  intro 
h: P ∨ Q
h
P, Q: Prop
h: P ∨ Q
Q ∨ P
  cases 
h: P ∨ Q
h with
P, Q: Prop
h: P ∨ Q
Q ∨ P
  | 
inl: ∀ {a b : Prop}, a → a ∨ b
inl 
hp: P
hp =>
P, Q: Prop
hp: P
inl
Q ∨ P
    right
P, Q: Prop
hp: P
inl.h
P
    exact 
hp: P
hp
Goals accomplished! 🐙
  | 
inr: ∀ {a b : Prop}, b → a ∨ b
inr 
hq: Q
hq =>
P, Q: Prop
hq: Q
inr
Q ∨ P
    left
P, Q: Prop
hq: Q
inr.h
Q
    exact 
hq: Q
hq
Goals accomplished! 🐙

Next up Level 8