My post was mainly adding agreement to yours with more specifics, "you" used is the "generic you".
> it is a distraction from learning undergraduate mathematics
Arguably so is LaTeX. But it's desirable that students (or just people learning the same material, later) spend some of their undergraduate time learning new things, right? And not just because it's new, but hopefully because it's better. Learning new/different things is just a small step further beyond learning old things with new/different assistants. And maybe some things will have to be cut out, like 17th century prose-proofs (edit: and even just moving to structured proofs without full formal tools is an improvement...), or square roots by hand (http://www.theodoregray.com/BrainRot/)
> it is a distraction from learning undergraduate mathematics
Arguably so is LaTeX. But it's desirable that students (or just people learning the same material, later) spend some of their undergraduate time learning new things, right? And not just because it's new, but hopefully because it's better. Learning new/different things is just a small step further beyond learning old things with new/different assistants. And maybe some things will have to be cut out, like 17th century prose-proofs (edit: and even just moving to structured proofs without full formal tools is an improvement...), or square roots by hand (http://www.theodoregray.com/BrainRot/)