Timothy Chow gave a fine answer in the context of classical mathematics. Here are some further sources for you to ponder. These not only work without choice, but also without excluded middle:

* [Homotopy Type Theory: Univalent Foundations of Mathematics](https://homotopytypetheory.org/book/). For instance, is [Blakers-Massey theorem](https://en.wikipedia.org/wiki/Blakers–Massey_theorem) advanced enough to count as real math?

* [C-CoRN](https://github.com/coq-community/corn) library, skim the README or see [this paper](https://www.cs.ru.nl/~herman/PUBS/ccorn.pdf) for a humane summary of what is in it.

* [UniMath](https://github.com/UniMath/UniMath) library, inititiated by the late Vladimir Voevodsky, browse [this folder](https://github.com/UniMath/UniMath/tree/master/UniMath) to get a feel for what is in it.

The moral of the story is that the folk tales that mathematicians tell about how choice-free mathematics is completely different, or even impoverished beyond recognition, are just folk tales. Of course, one has to be a bit more careful, but that is always the case when we generalize, as new phenomena arise.