which subterm needs an axiom

Stream: general

[Yury G. Kudryashov]

Is there an easy way to find out which part(s) of a proof depend on classical.choice?

[Bryan Gin-ge Chen]

The closest thing I know of is @Mario Carneiro's snippet here which gets the axioms used by a declaration. Maybe you could use that to inspect the terms generated at various points in the proof?

[Bryan Gin-ge Chen]

(It'd be nice to have something like this in mathlib, though I suspect that adding more Lean 3 meta code probably isn't a high priority at the moment.)