Week 2: Following a proof step by step🔗

Tactic proofs and the goal display: intro, exact, constructor, cases, witnesses, apply, have, rewriting, and what automation does (and does not) tell you.

1. Day 8: Proofs are step by step
2. Day 9: intro and exact
3. Day 10: Taking apart and building “and”
4. Day 11: Or and there-exists
5. Day 12: Using other theorems
6. Day 13: Rewriting and automation
7. Day 14: Week 2 review: a proof is a story