The Mechanics of Proof
1. Proofs by calculation 1.1. Proving equalities 1.2. Proving equalities in Lean 1.3. Tips and tricks 1.4. Proving inequalities 1.5. A shortcut 2. Proofs with structure 2.1. Intermediate steps 2.2. Invoking lemmas 2.3. “Or” and proof by cases 2.4. “And” 2.5. Existence proofs 3. Parity and divisibility 3.1. Definitions; parity 3.2. Divisibility 3.3. Modular arithmetic: theory 3.4. Modular arithmetic: calculations 3.5. Bézout’s identity 4. Proofs with structure, II 4.1. “For all” and implication 4.2. “If and only if” 4.3. “There exists a unique” 4.4. Contradictory hypotheses 4.5. Proof by contradiction 5. Logic 5.1. Logical equivalence 5.2. The law of the excluded middle 5.3. Normal form for negations 6. Induction 6.1. Introduction 6.2. Recurrence relations 6.3. Two-step induction 6.4. Strong induction 6.5. Pascal’s triangle 6.6. The Division Algorithm 6.7. The Euclidean algorithm 7. Number theory 7.1. Infinitely many primes 7.2. Gauss’ and Euclid’s lemmas 7.3. The square root of two 8. Functions 8.1. Injectivity and surjectivity 8.2. Bijectivity 8.3. Composition of functions 8.4. Product types 9. Sets 9.1. Introduction 9.2. Set operations 9.3. The type of sets 10. Relations 10.1. Reflexive, symmetric, antisymmetric, transitive 10.2. Equivalence relations
