This one is not just in Dummit and Foote; it's just too easy to miss. I'd guess it appears in half the places that state this result. Fixed it in my own lecture notes a few months ago.
It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.
After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.
After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.
https://github.com/ityonemo/bpa
Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language