order

order タクティクは、順序関係を扱うための専用のタクティクです。Preorder クラスや PartialOrder, LinearOrder クラスのインスタンスに対して使用することができます。

import Mathlib.Tactic.Order

section
  /- ## Preorder に対して使用する例 -/

  variable {α : Type} [Preorder α] (a b c d : α)

  example (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
    order

  example (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) : a ≤ d := by
    order

  example (h1 : a ≤ b) (h2 : ¬ (a < b)) : b ≤ a := by
    order
end

section
  /- ## PartialOrder に対して使用する例 -/

  variable {α : Type} [PartialOrder α] (a b c d : α)

  example (h1 : a ≤ b) (h2 : ¬ (a < b)) : a = b := by
    order

  example : ¬ (a < a) := by
    order
end

section
  /- ## LinearOrder に対して使用する例 -/

  variable {α : Type} [LinearOrder α] (a b c d : α)

  example (h1 : ¬ (a < b)) (h2 : ¬ (b < a)) : a = b := by
    order
end