mathlib

f7698588 - feat(tactic/push_neg): option for an alternate normal form of `¬ (P ∧ Q)` (#16586)

feat(tactic/push_neg): option for an alternate normal form of `¬ (P ∧ Q)` (#16586) Backport a feature of the [mathlib4 version](https://github.com/leanprover-community/mathlib4/pull/344) of `push_neg`: an option to make `¬ (P ∧ Q)` be normalized to `¬ P ∨ ¬ Q`, rather than `P → ¬ Q`. That was actually the original behaviour, but it was changed in #3362. I have implemented this as a global option `trace.push_neg.use_distrib` (using the [tracing option hack](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/custom.20options)) rather than as a piece of configuration information which is passed when using the tactic, because I imagine this feature will mostly be used in teaching (that was both my motivation and also @PatrickMassot's when he wrote the original version), where it is convenient to "set it and forget it". This is also how it is implemented in the mathlib4 version (cc @dupuisf @j-loreaux). Zulip: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/alternative.20normal.20form.20for.20push_neg