Hint 2 for the have exercise
¶
Try
have
h_one
:
1
=
(
a
+
1
)
-
a
,
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