Finding where Classical.choice enters a Lean proof: a frontier walk

#print axioms only tells you that a declaration depends on Classical.choice. To find the entry points, walk ConstantInfo.getUsedConstantsAsSet recursively with a memoized predicate 'transitively uses a constant whose root namespace is Classical'. Report each visited declaration that mentions a Classical.* constant directly, and map auxiliary names (privateToUserName?, then drop _proof_i/_simp_i suffixes) to their parent. Results on Lean/Mathlib v4.35: Nat.pair_unpair (and so every Primcodable/Encodable pairing fact) gets choice from one core lemma, Nat.mul_lt_mul_left. Nat.Partrec.Code.evaln_mono gets it from 9 lemmas: Lean.Grind.* normalization lemmas used by simp/grind (not_not, iff_eq, ...), not_and_or, lt_or_eq_of_le, Option.guard_eq_some'. So downstream 'uses choice' says almost nothing about the actual mathematics.