import MyNat.Definition
namespace MyNat
open MyNat

Proposition world.

Level 8 : (P → Q) → (¬ Q → ¬ P)

There is a false proposition false, with no proof. It is easy to check that ¬ Q is equivalent to Q ⟹ false, and in this tutorial we call this

not_iff_imp_false (P : Prop) : ¬ P ↔ (P → false)

which we can prove here using the simp tactic:

theorem 
not_iff_imp_false: ∀ (P : Prop), ¬P ↔ P → false = true
not_iff_imp_false (
P: Prop
P : 
Prop: Type
Prop) : ¬ 
P: Prop
P ↔ (
P: Prop
P → 
false: Bool
false) :=
  
P: Prop
¬P ↔ P → false = true
 
Goals accomplished! 🐙

So you can start the proof of the contrapositive below with

repeat rw [not_iff_imp_false]

to get rid of the two occurrences of ¬, and I'm sure you can take it from there. At some point your goal might be to prove false. At that point I guess you must be proving something by contradiction. Or are you?

Lemma : contrapositive

If P and Q are propositions, and P⟹ Q, then ¬ Q⟹ ¬ P.

lemma 
contrapositive: ∀ (P Q : Prop), (P → Q) → ¬Q → ¬P
contrapositive (
P: Prop
P 
Q: Prop
Q : 
Prop: Type
Prop) : (
P: Prop
P → 
Q: Prop
Q) → (¬ 
Q: Prop
Q → ¬ 
P: Prop
P) := 
P, Q: Prop
(P → Q) → ¬Q → ¬P

  
P, Q: Prop
(P → Q) → ¬Q → ¬P
 
P, Q: Prop
(P → Q) → ¬Q → ¬P
P, Q: Prop
(P → Q) → (Q → false = true) → P → false = true
P, Q: Prop
(P → Q) → (Q → false = true) → ¬P

  
P, Q: Prop
f: P → Q
(Q → false = true) → P → false = true

  
P, Q: Prop
f: P → Q
h: Q → false = true
P → false = true

  
P, Q: Prop
f: P → Q
h: Q → false = true
p: P
false = true

  
P, Q: Prop
f: P → Q
h: Q → false = true
p: P
Q

  
P, Q: Prop
f: P → Q
h: Q → false = true
p: P
P

  
Goals accomplished! 🐙

Technical note

All of that rewriting you did with rw in addition world was rewriting hypothesis of the form h : X = Y, but you can also rw [h] if h : P ↔ Q (because propositional extensionality says that if P ⟺ Q then P = Q, and mathematicians use this whether or not they notice.)

Next up Level 9