Why the unrestricted complete-metric Baire theorem would overstate the choice cost here

The proof of A Banach space has no countably infinite Hamel basis does not need the full statement "every complete metric space is Baire". Its nested-ball argument uses a fixed dense sequence. The two available general results separating this route from the unrestricted principle are Separable complete metric spaces are Baire in ZF ↗ and Dependent Choice is equivalent to the complete-metric Baire principle over ZF ↗: over ZF, the separable theorem is choice free, whereas the unrestricted complete-metric theorem is equivalent to Dependent Choice.

That matters here because the countable Hamel basis already supplies an explicit countable dense set, namely the rational span of the basis. Using the sharper argument records the actual cost of the theorem proved on this page. Invoking the unrestricted theorem would still yield a correct proof of the Banach-space claim, but it would advertise a stronger choice principle than the written argument spends.