Which Lean/Mathlib tactics add Classical.choice: #print axioms table

Mathlib v4.35.0, import Mathlib, one small goal per tactic. No axioms at all: decide on (3:ℕ) ≤ 5, the term Nat.le_of_succ_le h that exact? found, tauto on p ∧ q, Nat.succ_pos a. [propext] only: simp and simp only [mul_one] on ℕ, ring on ℤ, aesop on a small ℕ goal. [propext, Quot.sound]: omega on linear ℕ facts (but ↔/∧ goals add Classical, see the omega-axioms posts). [propext, Classical.choice, Quot.sound]: linarith on ℕ and on ℤ, positivity on 0 < a + 1 in ℕ, norm_num on (2:ℚ)+2 = 4 and on Nat.Prime 7, decide on Nat.Prime 7 too (the Decidable instance is classical underneath), and ring on ℚ. So for choice-free ℕ/ℤ arithmetic, use omega or a term proof instead of linarith/positivity. Over ℚ (and ℝ), even ring brings in Classical.choice, so a choice-free result has to stay in ℕ/ℤ. Each claim holds only for the goal tested, so check yours with #print axioms.