You write, "we shouldn't need the axiom of choice to define the derivative."
The good news is that we don't!
Only model-theoretic approaches, which justify the infinitesimal methods by constructing a hyperreal field, require (a weak form of) the axiom of choice [2].
However, there are axioms for nonstandard analysis which are conservative over the usual choice-free set theory ZF. The three axioms of Hrbacek and Katz presented in the article "Infinitesimal analysis without the Axiom of Choice" [1] are the best recent example: these axioms allow you to do everything that is done in Keisler's book and more (including defining the derivative), and you never need to invoke the axiom of choice to justify them.
[1] https://arxiv.org/abs/2009.04980
[2] Essentially, the set of properties satisfied by a fixed nonstandard hypernatural gives rise to a non-principal ultrafilter over the naturals. The axiom of choice is necessary to prove the existence of non-principal ultrafilters in (choice-free) set theory, but the existence of non-principal ultrafilters is not sufficient to prove the axiom of choice.
The good news is that we don't!
Only model-theoretic approaches, which justify the infinitesimal methods by constructing a hyperreal field, require (a weak form of) the axiom of choice [2].
However, there are axioms for nonstandard analysis which are conservative over the usual choice-free set theory ZF. The three axioms of Hrbacek and Katz presented in the article "Infinitesimal analysis without the Axiom of Choice" [1] are the best recent example: these axioms allow you to do everything that is done in Keisler's book and more (including defining the derivative), and you never need to invoke the axiom of choice to justify them.
[1] https://arxiv.org/abs/2009.04980
[2] Essentially, the set of properties satisfied by a fixed nonstandard hypernatural gives rise to a non-principal ultrafilter over the naturals. The axiom of choice is necessary to prove the existence of non-principal ultrafilters in (choice-free) set theory, but the existence of non-principal ultrafilters is not sufficient to prove the axiom of choice.