The Hauptvermutung is so obvious that it gets taken for granted everywhere, and most of us learn algebraic topology without ever noticing this huge gap in its foundations (of the text-book standard simplicial approach). It is implicit every time one states that a homotopy invariant of a simplicial complex, such as simplicial homology, is in fact a homotopy invariant of a polyhedron.
I have to admit I find this statement mystifying. We recently set up the theory of simplicial homology in lecture and I do not see anywhere that the Hauptvermutung needs to be assumed to show that simplicial homology is a homotopy invariant. Doesn't this follow once you have simplicial approximation and you also know that simplicial maps which are homotopic induce chain-homotopic maps on simplicial chains?