Documentation

Mathlib.Tactic.Order.Preprocessing

Facts preprocessing for the order tactic #

In this file we implement the preprocessing procedure for the order tactic. See Mathlib.Tactic.Order for details of preprocessing.

source
theorem Mathlib.Tactic.Order.not_lt_of_not_le {α : Type u} [Preorder α] {x y : α} (h : ¬x ≤ y) :
¬x < y
source
theorem Mathlib.Tactic.Order.le_of_not_lt_le {α : Type u} [Preorder α] {x y : α} (h1 : ¬x < y) (h2 : x ≤ y) :
y ≤ x
source
def Mathlib.Tactic.Order.preprocessFactsPreorder (g : Lean.MVarId) (facts : Array AtomicFact) :
Lean.MetaM (Array AtomicFact)

Preprocesses facts for preorders. Replaces x < y with two equivalent facts: x ≤ y and ¬ (y ≤ x). Replaces x = y with x ≤ y, y ≤ x and removes x ≠ y.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Tactic.Order.preprocessFactsPartial (g : Lean.MVarId) (facts : Array AtomicFact) :
    Lean.MetaM (Array AtomicFact)

    Preprocesses facts for partial orders. Replaces x < y, ¬ (x ≤ y), and x = y with equivalent facts involving only ≤, ≠, and ≮.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mathlib.Tactic.Order.preprocessFactsLinear (g : Lean.MVarId) (facts : Array AtomicFact) :
      Lean.MetaM (Array AtomicFact)

      Preprocesses facts for linear orders. Replaces x < y, ¬ (x ≤ y), ¬ (x < y), and x = y with equivalent facts involving only ≤ and ≠.

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