Contraposition Proof

Stream: new members

[Cameron Crossman]

I am a new user and I am just getting my bearings with the platform. Would someone be able to walk me through a proof of Contraposition written in Lean? (p → q) → (¬q → ¬p). Much appreciated! I know the general steps but am getting confused about how to translate that into Lean.
(p → q)
¬(p ^ ¬q)
¬( ¬q ^ p)
r = ¬q, s = ¬p substitution
¬(r ^ ¬s )
(r → s)
substitute back in
¬q → ¬p

[Kevin Buzzard]

In tactic mode? If you keep using the intro tactic you will find yourself with hypotheses p->q, not q and p and with a goal of false. Now apply your hypotheses until you're done. Sorry, on phone and just off to bed, hope this helps

[Mario Carneiro]

Lean's logic is similar to natural deduction, where ¬p means p -> false so the proof is actually a lot easier than the one you sketched

[Bryan Gin-ge Chen]

Here's the proof in lean core, called "mt" for "modus tollens".

[Cameron Crossman]

Thank you!