fix(push_neg): preserve binder names (#31212)

This PR fixes the `push_neg` tactic so that it preserves binder names when pushing through `Exists`. It was previously picking up the `x` name from `∃ x, s x`, so spelling it as `Exists s` fixes the problem.

Author: JovanGerb

Mathlib/Tactic/Push.lean

@@ -30,7 +30,7 @@ attribute [push ←] ne_eq
 
 @[push] theorem not_iff : ¬ (p ↔ q) ↔ (p ∧ ¬ q) ∨ (¬ p ∧ q) :=
   _root_.not_iff.trans <| iff_iff_and_or_not_and_not.trans <| by rw [not_not, or_comm]
-@[push] theorem not_exists : (¬ ∃ x, s x) ↔ (∀ x, binderNameHint x s <| ¬ s x) :=
+@[push] theorem not_exists : (¬ Exists s) ↔ (∀ x, binderNameHint x s <| ¬ s x) :=
   _root_.not_exists
 
 -- TODO: lemmas involving `∃` should be tagged using `binderNameHint`,

MathlibTest/push_neg.lean

@@ -224,3 +224,8 @@ example {p q : Nat} : ¬ g.Adj p q := by
   exact test_sorry
 
 end no_proj
+
+-- test that binder names are preserved by `push_neg`
+/-- info: ∀ (a b : ℕ), ∃ c d, a + b ≠ c + d -/
+#guard_msgs in
+#push_neg ¬ ∃ a b : Nat, ∀ c d : Nat, a + b = c + d