Hint 1 for the barber paradox
¶
Try
rintro
h
,
cases
h
barber
with
h1
h2
,
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