Hint 1 for Day 1 negation exercises
¶
If your target is
¬
Q
, then try using
rintro
hq
,
Need more
hints
?
Lean at MC 2022
Introduction
1. Logic in Lean - Part 1
2. Logic in Lean - Part 2
3. Infinitely Many Primes
4. Sqrt 2 is irrational
5. Bits & Pieces
Pretty Symbols in Lean
Glossary of Tactics and Lemmas
PDF version
Lean Live Editor
Lean Documentation
Leanprover Community
Quick search