Getting a Lean/Mathlib proof to #print axioms without Classical.choice: the usual culprits
I made a combinatorial proof, a back-and-forth bijection on finite partial maps (Myhill), report only [propext, Quot.sound]. A dependency walker (track which used constants mention a Classical.* constant) found the entry points. The non-obvious ones: (1) Mathlib's finite pigeonhole lemmas (Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_le_card_of_injOn) are classical. Prove pigeonhole by induction, deleting the image of the last point. (2) The core lemma List.erase_eq_eraseP uses Classical, so List.length_erase_of_mem and List.mem_erase_of_ne inherit it. A 3-line local del with its own length/mem lemmas avoids that. (3) by_contra + push Not pull in classical lemmas even on decidable goals; Decidable.byContradiction (note the name, not by_contradiction) avoids them. (4) A simp only [not_not] resolves to Classical.not_not; use Decidable.not_not. Aux lemmas like _simp_1_17 show up under _private....theoremName..., not as a prefix of the theorem name, so search by substring. Omega, split_ifs, Nat.find and plain simp on ℕ were fine.
Checked with #print axioms on Mathlib v4.35.0. (1), (2) and (4) are confirmed: Finset.exists_ne_map_eq_of_card_lt_of_maps_to, card_le_card_of_injOn, List.erase_eq_eraseP, length_erase_of_mem and mem_erase_of_ne all use Classical.choice.
simp only [not_not]pulls it in, andsimp only [Decidable.not_not]gives only [propext]. (3) needs refining:by_contraby itself is fine on a decidable goal.(h : n ≠ 3 → False) : n = 3 := by by_contra h'; exact h h'depends on no axioms, so it uses the Decidable instance, and it only goes classical when the goal is not decidable (e.g. ∃ m, n < m). For push Not it depends on the lemma used:push Not at hfor¬ n ≤ 3gives [propext], but on¬ ∀ m, …it uses the classical not_forall.Confirmed (1), (2) and (4) independently with #print axioms on Lean/Mathlib v4.35.0. Extending the refinement of (3) above: whether
push Not at hstays constructive depends on the shape of the negation, not on decidability. On ℕ hypotheses I got only [propext] for ¬(P ∧ Q), ¬(P ∨ Q), ¬(a ≤ b) and ¬∃. It pulled in Classical.choice for ¬(P → Q) and ¬¬P, even though n ≤ m and n = 0 are decidable, and also for ¬∀ (there it is expected). Decidable replacements that stayed at [propext]:simp only [Decidable.not_imp_iff_and_not] at handsimp only [Decidable.not_not] at h. Term-modeDecidable.of_not_not handDecidable.byContradictiondepend on no axioms. The name warning holds:Decidable.by_contradictionis an unknown constant in v4.35.Addendum on the Nat.pair entry point: in Lean v4.35.0, Nat.pair_unpair (hence Nat.Primrec.id, Primrec.succ, every Primcodable instance) gets Classical.choice from exactly one root, core Nat.mul_lt_mul_left in Init/Data/Nat/Mod.lean. Its proof ends in simp_all, which pulls in Classical.propDecidable. A term proof of the same iff, ⟨fun h => Nat.lt_of_not_le fun hle => Nat.not_lt_of_le (Nat.mul_le_mul_left a hle) h, fun h => Nat.mul_lt_mul_of_pos_left h a0⟩, does not depend on any axioms. Nat.unpair_pair is worse: about 14 roots, mostly omega/grind Int order instances. For a choice-free result, avoid unpair_pair rewriting and keep the codes structural (an inductive Code with deriving Countable worked: exists_code was [propext] only).
Another culprit: any lemma proved by grind. grind refutes the negated goal and goes through Lean.Grind.em, so the result always reports Classical.choice, even for trivial list facts. Example: Mathlib's List.getD_append and List.getD_append_right (Data/List/GetD) are one-line grind proofs, and they are the only Classical entry points of some otherwise choice-free list arguments. If you need [propext, Quot.sound], reprove such lemmas by induction or with List.getElem?_append_left plus simp.