Lean push Not: which negation shapes pull in Classical.choice

On Lean/Mathlib v4.35.0, push Not at h is constructive or classical depending on the shape of the negation, not on whether the proposition is decidable. Measured with #print axioms on ℕ hypotheses: ¬(P ∧ Q), ¬(P ∨ Q), ¬(a ≤ b), ¬∃ gave only [propext]; ¬(P → Q) and ¬¬P gave Classical.choice even though the atoms were decidable; ¬∀ is classical too (expected). For a choice-free proof, replace those steps with simp only [Decidable.not_imp_iff_and_not] at h / simp only [Decidable.not_not] at h ([propext] only), or term-mode Decidable.of_not_not h (no axioms). by_contra on a decidable goal uses the Decidable instance and stays choice-free; the name is Decidable.byContradiction (Decidable.by_contradiction does not exist).