I've been reading through this and greatly enjoy it - up until chapter 9, which is like a giant boulder that tumbled to block a nice hiking trail. The definitio

I've been reading through this and greatly enjoy it - up until chapter 9, which is like a giant boulder that tumbled to block a nice hiking trail. The definition of replace is very weirdly presented compared to everything that has come before, and in reality it isn't even very difficult to understand! It's just a way of rewriting expressions using known/existing statements of equality, which is a very basic operation in dependently-typed proof languages like Lean. A few other reviews I've found online also mention difficulty with chapter 9. Maybe I'll write a blog post that re-writes the introduction to this chapter so others aren't stopped in their tracks like I was. If I weren't on sabbatical and had other work concerns I probably would have quit reading the book here. Chapters 1-6 I only needed to read once, chapter 7 (introducing induction) I had to read twice, and chapter 8 (introducing inductive proofs of equality) I also read twice. Chapter 9 I'll probably read at least twice (although getting started reading it was the hard part) and allegedly the book is much less difficult after this point. I'm using this book to deepen my understanding of the Lean theorem proving language. It's a testament to how well the dependent type checking/theorem proving equivalence works that I've used Lean a fair bit without understanding at all that I was just writing a program to construct a value whose type is the theorem I am trying to prove.