It helps to state carefully what you are trying to achieve. I want a theorem prover where constructing numbers such that ℕ ⊂ ℤ is easy. Doing this in a theorem prover is not trivial, for example none of the type based theorem provers allow that (although, Isabelle/ZF might qualify; it is based on set theory on top of a weak intuitionistic type theory; but here ℕ and ℤ are not types, but sets of the same type). It is trivial though if you are a mathematician, no matter what you are working on. You know that these constructions can be done, and that as a result you can assume ℕ ⊂ ℤ (if you want to). So as long as your theorem prover doesn't support something as trivial as that, it is lacking.
And yes, that is exactly what Buzzard is talking about. For the case I am talking about here though, that is just table stakes: make sure your prover can do ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. If you can do that, you can start worrying about more advanced issues of equality, and you might find that you have already solved a significant amount of them.
I can confirm that in Isabelle/ZF one can set up a context (locale) with the meaning of the ℕ ℤ ℝ ℂ symbols defined so that ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. However ℕ for example will not be equal in such case to the canonical set of ZF natural numbers where 1 = {0}, 2 = {0,1} etc.
And yes, that is exactly what Buzzard is talking about. For the case I am talking about here though, that is just table stakes: make sure your prover can do ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. If you can do that, you can start worrying about more advanced issues of equality, and you might find that you have already solved a significant amount of them.