If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest of the book.
I loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalization could become if it strayed too far from Mathlib — but also was worried about losing the self-contained-ness if it just used Mathlib. This is a nice compromise imo.
