import Mathlib.Tactic.LeftRight
import Mathlib.Tactic.Basic
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Cases
import PropositionWorld.Level8 -- not_iff_imp_false

Advanced proposition world.

You already know enough to embark on advanced addition world. But here are just a couple more things.

Level 9: exfalso and proof by contradiction.

It's certainly true that P ∧ (¬ P) ⟹ Q for any propositions P and Q, because the left hand side of the implication is false. But how do we prove that false implies any proposition Q? A cheap way of doing it in Lean is using the exfalso tactic, which changes any goal at all to false. You might think this is a step backwards, but if you have a hypothesis h : ¬ P then after rw not_iff_imp_false at h, you can apply h, to make progress.

Lemma

If P and Q are true/false statements, then (P ∧ (¬ P)) ⟹ Q.

lemma 
contra: ∀ (P Q : Prop), P ∧ ¬P → Q
contra (
P: Prop
P 
Q: Prop
Q : 
Prop: Type
Prop) : (
P: Prop
P ∧ ¬ 
P: Prop
P) → 
Q: Prop
Q := by
P, Q: Prop
P ∧ ¬P → Q
  intro 
h: P ∧ ¬P
h
P, Q: Prop
h: P ∧ ¬P
Q
  cases 
h: P ∧ ¬P
h with
P, Q: Prop
h: P ∧ ¬P
Q
  | 
intro: ∀ {a b : Prop}, a → b → a ∧ b
intro 
p: P
p 
np: ¬P
np =>
P, Q: Prop
p: P
np: ¬P
intro
Q
    exfalso
P, Q: Prop
p: P
np: ¬P
intro.h
False
    apply 
np: ¬P
np
P, Q: Prop
p: P
np: ¬P
intro.h
P
    assumption
Goals accomplished! 🐙

Pro tip.

¬ P is actually P → false by definition and since np: ¬ P is a hypothesis, apply q changes ⊢ False to ⊢ P. Neat trick. We started with ⊢ Q, but could not prove it so we jumped to False so we could use np: ¬ P to get to the desired goal ⊢ P.

Next up Level 10