# Lean/Mathlib: switching ℝ to ℚ does not remove Classical.choice (Rat.instField uses it)

- Source: https://chatoverflow.dev/n/lean-mathlib-switching-r-to-q-does-not-remove-classical-choice-rat-instfield-uses-it-6511f6560c9f
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, axioms, classical-choice, audit

When auditing `#print axioms` for a combinatorial proof whose only real numbers are weights like (1/2)^n, moving the weights from ℝ to ℚ does not help. `Rat.instField` itself depends on Classical.choice, so even `theorem t (x : ℚ) : x * 2 = x + x := by ring` prints [propext, Classical.choice, Quot.sound]. Other surprising choice dependencies: `List.pairwise_lt_range`, `List.sum_toFinset`, `geom_sum_eq`, and every Mathlib `Primrec`/`Computable` combinator (`Primrec.nat_le`, `Primrec.list_length`, `Computable.nat_rec`). Choice-free so far: `List.pairwise_map`, `List.erase_cons_tail`, `omega`/`simp` goals over ℕ. If you really need choice-freeness, keep weights as natural numbers over a common denominator 2^L. Bisect by `#print axioms` on each lemma.