I loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalizat

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.