Specializations of basic logic lemmas

These are useful for omega while constructing proofs, but not considered generally useful so are hidden in the Std.Tactic.Omega namespace.

If you find yourself needing them elsewhere, please move them first to Std.Logic.

theorem Std.Tactic.Omega.and_not_not_of_not_or {p : Prop} {q : Prop} : ¬(p ∨ q) → ¬p ∧ ¬q

Alias of the forward direction of not_or.

theorem Std.Tactic.Omega.Decidable.or_not_not_of_not_and (p : Prop) (q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬(p ∧ q) → ¬p ∨ ¬q

Alias of the forward direction of Decidable.not_and_iff_or_not.

theorem Std.Tactic.Omega.Decidable.and_or_not_and_not_of_iff {a : Prop} {b : Prop} [Decidable b] : (a ↔ b) → a ∧ b ∨ ¬a ∧ ¬b

Alias of the forward direction of Decidable.iff_iff_and_or_not_and_not.

theorem Std.Tactic.Omega.Decidable.not_iff_iff_and_not_or_not_and {a : Prop} {b : Prop} [Decidable a] [Decidable b] : ¬(a ↔ b) ↔ a ∧ ¬b ∨ ¬a ∧ b

theorem Std.Tactic.Omega.Decidable.and_not_or_not_and_of_not_iff {a : Prop} {b : Prop} [Decidable a] [Decidable b] : ¬(a ↔ b) → a ∧ ¬b ∨ ¬a ∧ b

Alias of the forward direction of Std.Tactic.Omega.Decidable.not_iff_iff_and_not_or_not_and.

theorem Std.Tactic.Omega.Decidable.and_not_of_not_imp {a : Prop} {b : Prop} [Decidable a] : ¬(a → b) → a ∧ ¬b

Alias of the forward direction of Decidable.not_imp.