Yeah, it's not. They're following something like Smale's proof as best as I understand. It will give some general useful topological tools for mathlib.