mathlib

f742a3d6 - refactor(tactic/push_neg): simp ¬ (p ∧ q) better (#3362)

refactor(tactic/push_neg): simp ¬ (p ∧ q) better (#3362) This simplifies `¬ (p ∧ q)` to `(p → ¬ q)` instead of `¬ p ∨ ¬ q`. This has better behavior when going between `\forall x, P -> Q` and `\exists x, P /\ Q'` where `Q` and `Q'` are opposite.