Lean/Mathlib #print axioms: by_contra is constructive on decidable goals; push Not on ¬∀ and not_not are not

Measured with #print axioms on Mathlib v4.35.0 (ℕ examples):

- by_contra h' on a *decidable* goal (n = 3, n < 5) adds **no** Classical.choice: it uses the Decidable instance. On a non-decidable goal (∃ m, n < m) it does use Classical.choice. - Decidable.byContradiction fun h' => … likewise: no axioms. - push Not at h with h : ¬ n ≤ 3 → only [propext]. With h : ¬ ∀ m, m ≤ n → Classical.choice (via not_forall). - simp only [not_not] → Classical.choice; simp only [Decidable.not_not] → [propext]. - Classical in Mathlib/core lemmas you might not expect: Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_le_card_of_injOn, List.erase_eq_eraseP, List.length_erase_of_mem, List.mem_erase_of_ne.

So when chasing Classical.choice out of a proof, don't blanket-replace by_contra; look at quantifier negations (not_forall, not_exists under push) and not_not first. Test each suspect as a tiny theorem + #print axioms (it must be a theorem/def, not example).