push_neg for eventually quantifiers

Stream: mathlib4

[Lorenzo Luccioli]

In the example below 'push_neg' does not manage to push the negation inside the Eventually quantifier.
It would seem natural for it to be able to handle cases like this one (and analogous cases with the Frequently quantifier), to avoid having to use lemmas like 'Filter.not_eventually' manually.

import Mathlib.Order.Filter.Basic

example (f : Filter Nat) (h : ∃ᶠ x in f, x = 0) : ¬ ∀ᶠ x in f, x ≠ 0 := by
  push_neg
  -- push_neg does nothing
  -- ⊢ ¬∀ᶠ (x : ℕ) in f, x ≠ 0
  apply Filter.not_eventually.mpr
  -- ⊢ ∃ᶠ (x : ℕ) in f, ¬x ≠ 0
  push_neg
  exact h

Actually in this case 'simp' solves the problem, but I guess there are situations where one just wants to move the negations without having 'simp' change other details.

example (f : Filter Nat) (h : ∃ᶠ x in f, x = 0) : ¬ ∀ᶠ x in f, x ≠ 0 := by
  simp
  exact h

[Alex J. Best]

push_neg is basically one big lookup table https://github.com/leanprover-community/mathlib4/blob/e8433a6b8e7980bfaaf9b34513b77da2af14995a/Mathlib/Tactic/PushNeg.lean#L76 so implementing this feature would be a great first example for someone who wanted to try metaprogramming out

There is the slight issue of dependencies however, the way push_neg is implemented unfortunately seems to require all the targeted pushes to be imported in the tactic itself, I suppose this is not strictly necessary but a better extension mechanism would help for sure