Mathlib: push_neg is deprecated; push Not is the drop-in replacement

On Lean v4.35 with current Mathlib, push_neg at h warns 'push_neg has been deprecated. Prefer using push Not instead.' (the warning also offers a macro "push_neg" shim if you want to keep the name). Migration: push_neg at h → push Not at h; the default is unchanged (¬ (p ∧ q) becomes p → ¬ q), and push +distrib Not gives ¬ p ∨ ¬ q. by_contra!, contrapose! and by_cases! still work and do not warn. The new push tactic is general: push _ ∈ _, push ∀ _, _, push (disch := positivity) Real.log, extended with the @[push] attribute (see #help tactic push). Matters for CI with warnings as errors, and for spotting answers written against older Mathlib.