# Documentation

Mathlib.Tactic.PushNeg

theorem Mathlib.Tactic.PushNeg.not_and_eq (p : Prop) (q : Prop) :
(¬(p q)) = (p¬q)
theorem Mathlib.Tactic.PushNeg.not_forall_eq {α : Sort u_1} (s : αProp) :
(¬((x : α) → s x)) = x, ¬s x
theorem Mathlib.Tactic.PushNeg.not_exists_eq {α : Sort u_1} (s : αProp) :
(¬x, s x) = ∀ (x : α), ¬s x
theorem Mathlib.Tactic.PushNeg.not_implies_eq (p : Prop) (q : Prop) :
(¬(pq)) = (p ¬q)
theorem Mathlib.Tactic.PushNeg.not_ne_eq {α : Sort u_1} (x : α) (y : α) :
(¬x y) = (x = y)
theorem Mathlib.Tactic.PushNeg.not_le_eq {β : Type u} [inst : ] (a : β) (b : β) :
(¬a b) = (b < a)
theorem Mathlib.Tactic.PushNeg.not_lt_eq {β : Type u} [inst : ] (a : β) (b : β) :
(¬a < b) = (b a)

Make push_neg use not_and_distrib rather than the default not_and.

Push negations at the top level of the current expression.

Equations
• One or more equations did not get rendered due to their size.

Recursively push negations at the top level of the current expression. This is needed to handle e.g. triple negation.

Common entry point to push_neg as a conv.

Equations
• One or more equations did not get rendered due to their size.

Push negations into the conclusion of an expression. For instance, an expression ¬ ∀ x, ∃ y, x ≤ y¬ ∀ x, ∃ y, x ≤ y∀ x, ∃ y, x ≤ y∃ y, x ≤ y≤ y will be transformed by push_neg into ∃ x, ∀ y, y < x∃ x, ∀ y, y < x∀ y, y < x. Variable names are conserved. This tactic pushes negations inside expressions. For instance, given a hypothesis

| ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
≤ δ → |f x - y₀| ≤ ε)
→ |f x - y₀| ≤ ε)
≤ ε)


writing push_neg will turn the target into

| ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
→ (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
≤ δ ∧ ε < |f x - y₀|),
∧ ε < |f x - y₀|),


(The pretty printer does not use the abreviations ∀ δ > 0∀ δ > 0 and ∃ ε > 0∃ ε > 0 but this issue has nothing to do with push_neg).

Note that names are conserved by this tactic, contrary to what would happen with simp using the relevant lemmas.

This tactic has two modes: in standard mode, it transforms ¬(p ∧ q)¬(p ∧ q)∧ q) into p → ¬q→ ¬q¬q, whereas in distrib mode it produces ¬p ∨ ¬q¬p ∨ ¬q∨ ¬q¬q. To use distrib mode, use set_option push_neg.use_distrib true.

Equations

Execute push_neg as a conv tactic.

Equations
• One or more equations did not get rendered due to their size.

The syntax is #push_neg e, where e is an expression, which will print the push_neg form of e.

#push_neg understands local variables, so you can use them to introduce parameters.

Equations
• One or more equations did not get rendered due to their size.

Execute main loop of push_neg at the main goal.

Equations
• One or more equations did not get rendered due to their size.

Execute main loop of push_neg at a local hypothesis.

Equations
• One or more equations did not get rendered due to their size.

Push negations into the conclusion of a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y¬ ∀ x, ∃ y, x ≤ y∀ x, ∃ y, x ≤ y∃ y, x ≤ y≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x∃ x, ∀ y, y < x∀ y, y < x. Variable names are conserved. This tactic pushes negations inside expressions. For instance, given a hypothesis

h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
≤ δ → |f x - y₀| ≤ ε)
→ |f x - y₀| ≤ ε)
≤ ε)


writing push_neg at h will turn h into

h : ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
→ (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
≤ δ ∧ ε < |f x - y₀|),
∧ ε < |f x - y₀|),


(The pretty printer does not use the abreviations ∀ δ > 0∀ δ > 0 and ∃ ε > 0∃ ε > 0 but this issue has nothing to do with push_neg).

Note that names are conserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can also use this tactic at the goal using push_neg, at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal using say push_neg at h h' ⊢⊢ as usual.

This tactic has two modes: in standard mode, it transforms ¬(p ∧ q)¬(p ∧ q)∧ q) into p → ¬q→ ¬q¬q, whereas in distrib mode it produces ¬p ∨ ¬q¬p ∨ ¬q∨ ¬q¬q. To use distrib mode, use set_option push_neg.use_distrib true.

Equations
• One or more equations did not get rendered due to their size.