Sure you can work around it most of the time, but some times you cant. The whole point is that isomorphic is not equality in set theory, and sometimes proofs does not transfer along isomorphism because they refer to implementations. I agree that it is much preferable to work with abstract structure, but that not always what happens in practice. The natural number example is contrived but easy to see. My point of view is also that I do not like the Lean approach. It would actually like no junk theorems to exist in my theory. I am much more partial to the univalent approach and in particular univalent implementation that compute e.g. cubical. Regarding how easy it is to formalize, you are right. Lots of good work happens with set theory based type theory. My point was also that set theoretic foundations themselves are very hard to formalize, e.g ZFC + logic is very difficult to work from. A pure type theoretical foundations is much easier to get of the ground from. To prove that plus commutes directly from ZFC is a nightmare.