awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using le_of_lt <| compare_lt_iff_lt.1 h

Premises used: le_of_lt, Iff.mp, compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using le_of_eq <| compare_eq_iff_eq.1 h

Premises used: compare_eq_iff_eq, Iff.mp, le_of_eq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using compare_gt_iff_gt.1 h

Premises used: compare_gt_iff_gt, Iff.mp
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.lt ↔ b ≤ a
eq : ∀ (h : compare a b = Ordering.eq), Ordering.eq ≠ Ordering.lt ↔ b ≤ a
gt : ∀ (h : compare a b = Ordering.gt), Ordering.gt ≠ Ordering.lt ↔ b ≤ a
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a

Tactic:
cases h : compare a b

Premises used: Ord.compare
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using compare_lt_iff_lt.1 h

Premises used: Iff.mp, compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h

Premises used: compare_eq_iff_eq, Iff.mp, le_of_eq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using le_of_lt <| compare_gt_iff_gt.1 h

Premises used: compare_gt_iff_gt, le_of_lt, Iff.mp
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
o : Ordering
lt : compare a b = Ordering.lt ↔ Ordering.lt.Compares a b
eq : compare a b = Ordering.eq ↔ Ordering.eq.Compares a b
gt : compare a b = Ordering.gt ↔ Ordering.gt.Compares a b
⊢ compare a b = o ↔ o.Compares a b

Tactic:
cases o
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : compare a b = Ordering.lt ↔ a < b
⊢ compare a b = Ordering.lt ↔ Ordering.lt.Compares a b

Tactic:
simp only [Ordering.Compares]

Premises used: Ordering.Compares
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
gt : compare a b = Ordering.gt ↔ a > b
⊢ compare a b = Ordering.gt ↔ Ordering.gt.Compares a b

Tactic:
simp only [Ordering.Compares]

Premises used: Ordering.Compares
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
compare_lt_iff_lt

Premises used: compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
exact compare_lt_iff_lt

Premises used: compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
compare_eq_iff_eq

Premises used: compare_eq_iff_eq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
exact compare_eq_iff_eq

Premises used: compare_eq_iff_eq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
compare_gt_iff_gt

Premises used: compare_gt_iff_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
exact compare_gt_iff_gt

Premises used: compare_gt_iff_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ cmp a b = compare a b

Tactic:
((compare_iff ..).2 ?_).symm

Premises used: Iff.mpr, Eq.symm, compare_iff
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
refine : (cmp a b).Compares a b
⊢ cmp a b = compare a b

Tactic:
refine ((compare_iff ..).2 ?_).symm

Premises used: Iff.mpr, Eq.symm, compare_iff
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b), Ordering.lt.Compares a b
pos₁ : ∀ (h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b) (h2 : (fun (x1 x2 : α) ↦ x1 < x2) b a), Ordering.gt.Compares a b
neg : ∀ (h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b) (h2 : ¬(fun (x1 x2 : α) ↦ x1 < x2) b a), Ordering.eq.Compares a b
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then Ordering.lt
      else if (fun (x1 x2 : α) ↦ x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b

Tactic:
split_ifs with h1 h2
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b
⊢ Ordering.lt.Compares a b

Tactic:
h1

Premises used: Ordering.Compares
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b
⊢ Ordering.lt.Compares a b

Tactic:
exact h1
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b
h2 : (fun (x1 x2 : α) ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

Tactic:
h2

Premises used: Ordering.Compares
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b
h2 : (fun (x1 x2 : α) ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

Tactic:
exact h2
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b
h2 : ¬(fun (x1 x2 : α) ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Premises used: le_antisymm, not_lt, Ordering.Compares, Iff.mp
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b
h2 : ¬(fun (x1 x2 : α) ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Premises used: le_antisymm, not_lt, Iff.mp
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ cmp a b = compareOfLessAndEq a b

Tactic:
(cmp_eq_compare ..).trans (LinearOrder.compare_eq_compareOfLessAndEq ..)

Premises used: cmp_eq_compare, LinearOrder.compare_eq_compareOfLessAndEq, Eq.trans
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
lt : compare b a = Ordering.lt → compare a b = Ordering.lt.swap
eq : compare b a = Ordering.eq → compare a b = Ordering.eq.swap
gt : compare b a = Ordering.gt → compare a b = Ordering.gt.swap
⊢ compare a b = (compare b a).swap

Tactic:
cases _ : compare b a

Premises used: Ord.compare
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
h : compare b a = Ordering.lt
⊢ compare a b = Ordering.lt.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Premises used: compare_eq_iff_eq, compare_gt_iff_gt, Ordering.swap, compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
h : compare b a = Ordering.eq
⊢ compare a b = Ordering.eq.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Premises used: compare_eq_iff_eq, compare_gt_iff_gt, Ordering.swap, compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
h : compare b a = Ordering.gt
⊢ compare a b = Ordering.gt.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Premises used: compare_eq_iff_eq, compare_gt_iff_gt, Ordering.swap, compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c a_1 b_1 c_1 : α
h₁ : (compare a_1 b_1).isLE = true
h₂ : (compare b_1 c_1).isLE = true
simp : ∀ (h₁ : a_1 ≤ b_1) (h₂ : b_1 ≤ c_1), a_1 ≤ c_1
⊢ (compare a_1 c_1).isLE = true

Tactic:
simp only [← Ordering.ne_gt_iff_isLE, compare_le_iff_le] at *

Premises used: Ordering.ne_gt_iff_isLE, compare_le_iff_le
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c a_1 b_1 c_1 : α
h₁ : a_1 ≤ b_1
h₂ : b_1 ≤ c_1
⊢ a_1 ≤ c_1

Tactic:
le_trans h₁ h₂

Premises used: le_trans
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c a_1 b_1 c_1 : α
h₁ : a_1 ≤ b_1
h₂ : b_1 ≤ c_1
⊢ a_1 ≤ c_1

Tactic:
exact le_trans h₁ h₂

Premises used: le_trans
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ ∀ {a b : α}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
simp [compare_eq_iff_eq]

Premises used: compare_eq_iff_eq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, compare x y = Ordering.lt ↔ x < y

Tactic:
simp [compare_lt_iff_lt]

Premises used: compare_lt_iff_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, (compare x y).isLE = true ↔ x ≤ y

Tactic:
simp [← Ordering.ne_gt_iff_isLE, compare_le_iff_le]

Premises used: Ordering.ne_gt_iff_isLE, compare_le_iff_le
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
⊢ ∀ (a : α), a ≤ a

Tactic:
Preorder.le_refl

Premises used: Preorder.le_refl
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ a ≤ a

Tactic:
le_refl a

Premises used: le_refl
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
Preorder.le_trans _ _ _

Premises used: Preorder.le_trans
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b c : α
⊢ b ≤ a → c ≤ b → c ≤ a

Tactic:
flip le_trans

Premises used: flip, le_trans
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
Preorder.lt_iff_le_not_ge _ _

Premises used: Preorder.lt_iff_le_not_ge
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a ≤ b
hba : ¬b ≤ a
⊢ a < b

Tactic:
lt_iff_le_not_ge.2 ⟨hab, hba⟩

Premises used: Iff.mpr, lt_iff_le_not_ge, And.intro
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a = b
rw rw₁ : b ≤ b
⊢ a ≤ b

Tactic:
rw [hab]
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
⊢ a ≤ b

Tactic:
(lt_iff_le_not_ge.1 hab).1

Premises used: lt_iff_le_not_ge, And.left, Iff.mp
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
⊢ ¬b ≤ a

Tactic:
(lt_iff_le_not_ge.1 hab).2

Premises used: lt_iff_le_not_ge, And.right, Iff.mp
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a ≤ b
⊢ ¬b < a

Tactic:
imp_not_comm.1 not_le_of_gt hab

Premises used: imp_not_comm, Iff.mp, not_le_of_gt
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ¬a < a

Tactic:
fun h ↦ not_le_of_gt h le_rfl

Premises used: le_rfl, not_le_of_gt, Not
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a < b
hbc : b ≤ c
⊢ a < c

Tactic:
lt_of_le_not_ge (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_gt hab (le_trans hbc hca)

Premises used: le_of_lt, lt_of_le_not_ge, not_le_of_gt, le_trans
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a ≤ b
hbc : b < c
⊢ a < c

Tactic:
lt_of_le_not_ge (le_trans hab (le_of_lt hbc)) fun hca ↦ not_le_of_gt hbc (le_trans hca hab)

Premises used: le_of_lt, lt_of_le_not_ge, not_le_of_gt, le_trans
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b c : α
⊢ a < b → b < c → a < c

Tactic:
fun h₁ h₂ => lt_of_lt_of_le h₁ (le_of_lt h₂)

Premises used: le_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ a ≠ b

Tactic:
fun he => absurd h (he ▸ lt_irrefl a)

Premises used: lt_irrefl, Eq.rec, absurd, Not
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ ¬b < a

Tactic:
fun h1 : b < a => lt_irrefl a (lt_trans h h1)

Premises used: lt_irrefl, lt_trans, Not
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b ∨ a = b
⊢ a ≤ b

Tactic:
h.elim le_of_lt le_of_eq

Premises used: le_of_lt, le_of_eq, Or.elim
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a = b ∨ a < b
⊢ a ≤ b

Tactic:
h.elim le_of_eq le_of_lt

Premises used: le_of_lt, le_of_eq, Or.elim
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (a < b ↔ b < a) ↔ (a ≤ b ↔ b ≤ a)

Tactic:
grind [= lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (a < b ↔ a ≤ b) ↔ (b < a ↔ b ≤ a)

Tactic:
grind [= lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (a < b ↔ b ≤ a) ↔ (b < a ↔ a ≤ b)

Tactic:
grind [= lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (b ≤ a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
grind
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_2
inst : LT α
a b : α
⊢ (b < a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b < a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
grind
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ≤ b → b ≤ a → a = b

Tactic:
PartialOrder.le_antisymm _ _

Premises used: PartialOrder.le_antisymm
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ b ≤ a → a ≤ b → a = b

Tactic:
flip le_antisymm

Premises used: flip, le_antisymm
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a = b ↔ a ≤ b ∧ b ≤ a

Tactic:
⟨fun e => ⟨le_of_eq e, le_of_eq e.symm⟩, fun ⟨h1, h2⟩ => le_antisymm h1 h2⟩

Premises used: le_antisymm, _private.0.le_antisymm_iff.match_1, And.intro, Iff.intro, le_of_eq, Eq.symm, Eq
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ≤ b → a ≠ b → a < b

Tactic:
fun h₁ h₂ =>
  lt_of_le_not_ge h₁ <| mt (le_antisymm h₁) h₂

Premises used: mt, le_antisymm, lt_of_le_not_ge
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
inst_1 : DecidableLE α
hab : a ≤ b
⊢ a < b ∨ a = b

Tactic:
if hba : b ≤ a then Or.inr (le_antisymm hab hba) else Or.inl (lt_of_le_not_ge hab hba)

Premises used: dite, le_antisymm, lt_of_le_not_ge, Or.inl, Or.inr
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
inst_1 : DecidableLE α
⊢ a ≤ b ↔ a < b ∨ a = b

Tactic:
⟨Decidable.lt_or_eq_of_le, le_of_lt_or_eq⟩

Premises used: Decidable.lt_or_eq_of_le, Iff.intro, le_of_lt_or_eq
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ≤ b → a < b ∨ a = b

Tactic:
open scoped Classical in Decidable.lt_or_eq_of_le

Premises used: Decidable.lt_or_eq_of_le
-- Module: Mathlib.Order.Defs.PartialOrder
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ≤ b ↔ a < b ∨ a = b

Tactic:
open scoped Classical in Decidable.le_iff_lt_or_eq

Premises used: Decidable.le_iff_lt_or_eq
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Trans r r r
⊢ IsTrans α r

Tactic:
⟨fun _ _ _ => Trans.trans⟩

Premises used: Trans.trans, IsTrans.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
lt : α → α → Prop
⊢ Equivalence lt ↔ IsEquiv α lt

Tactic:
⟨.of_equivalence, fun _ => .of_isEquiv lt⟩

Premises used: IsEquiv.of_equivalence, Iff.intro, Equivalence.of_isEquiv
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
⊢ ¬r a a

Tactic:
Std.Irrefl.irrefl a

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ r a a

Tactic:
Std.Refl.refl a

Premises used: Std.Refl.refl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
inst : IsTrans α r
⊢ r a b → r b c → r a c

Tactic:
IsTrans.trans _ _ _

Premises used: IsTrans.trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Symm r
⊢ r a b → r b a

Tactic:
Std.Symm.symm _ _

Premises used: Std.Symm.symm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Antisymm r
⊢ r a b → r b a → a = b

Tactic:
Std.Antisymm.antisymm _ _

Premises used: Std.Antisymm.antisymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Asymm r
⊢ r a b → ¬r b a

Tactic:
Std.Asymm.asymm _ _

Premises used: Std.Asymm.asymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Trichotomous r
⊢ ∀ (a b : α), r a b ∨ a = b ∨ r b a

Tactic:
fun _ _ ↦ Std.Trichotomous.rel_or_eq_or_rel_swap

Premises used: Std.Trichotomous.rel_or_eq_or_rel_swap
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ ∀ ⦃a : α⦄, ¬r a a

Tactic:
⟨(·.irrefl), .mk⟩

Premises used: Std.Irrefl.irrefl, Std.Irrefl.mk, Iff.intro
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Refl r ↔ ∀ ⦃a : α⦄, r a a

Tactic:
⟨(·.refl), .mk⟩

Premises used: Std.Refl.refl, Std.Refl.mk, Iff.intro
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_2
r : α → α → Prop
⊢ IsTrans α r ↔ ∀ ⦃a b c : α⦄, r a b → r b c → r a c

Tactic:
⟨(·.trans), .mk⟩

Premises used: IsTrans.mk, IsTrans.trans, Iff.intro
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Symm r ↔ ∀ ⦃a b : α⦄, r a b → r b a

Tactic:
⟨(·.symm), .mk⟩

Premises used: Std.Symm.mk, Std.Symm.symm, Iff.intro
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Antisymm r ↔ ∀ ⦃a b : α⦄, r a b → r b a → a = b

Tactic:
⟨(·.antisymm), .mk⟩

Premises used: Std.Antisymm.antisymm, Iff.intro, Std.Antisymm.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Asymm r ↔ ∀ ⦃a b : α⦄, r a b → ¬r b a

Tactic:
⟨(·.asymm), .mk⟩

Premises used: Iff.intro, Std.Asymm.mk, Std.Asymm.asymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Total r ↔ ∀ ⦃a b : α⦄, r a b ∨ r b a

Tactic:
⟨(·.total), .mk⟩

Premises used: Std.Total.total, Iff.intro, Std.Total.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Trichotomous r ↔ ∀ ⦃a b : α⦄, ¬r a b → ¬r b a → a = b

Tactic:
⟨(·.trichotomous), .mk⟩

Premises used: Std.Trichotomous.mk, Iff.intro, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
inst : IsTrans α r
inst_1 : Std.Irrefl r
⊢ Std.Asymm r

Tactic:
⟨fun a _b h₁ h₂ => absurd (_root_.trans h₁ h₂) (irrefl a)⟩

Premises used: trans, irrefl, absurd, Std.Asymm.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b c : α
inst : DecidableRel r
inst_1 : Irrefl r
a : α
⊢ ¬Decidable.decide (r a a) = true

Tactic:
simpa using irrefl a

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b c : α
inst : DecidableRel r
inst_1 : Refl r
a : α
⊢ Decidable.decide (r a a) = true

Tactic:
simpa using refl a

Premises used: Std.Refl.refl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c_1 : α
inst : DecidableRel r
inst_1 : IsTrans α r
a b c : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b c) = true → Decidable.decide (r a c) = true

Tactic:
simpa using trans a b c

Premises used: IsTrans.trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Symm r
a b : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b a) = true

Tactic:
simpa using symm a b

Premises used: Std.Symm.symm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b

Tactic:
simpa using h₁
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a

Tactic:
simpa using h₂
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Asymm r
a b : α
⊢ Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true

Tactic:
simpa using asymm a b

Premises used: Std.Asymm.asymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Total r
a b : α
⊢ Decidable.decide (r a b) = true ∨ Decidable.decide (r b a) = true

Tactic:
simpa using total a b

Premises used: Std.Total.total
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
inst : DecidableRel r
inst_1 : Trichotomous r
a b : α
⊢ ¬Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true → a = b

Tactic:
simpa using trichotomous a b

Premises used: Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
⊢ ¬r a a

Tactic:
irrefl a

Premises used: irrefl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ r a a

Tactic:
refl a

Premises used: refl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
inst : IsTrans α r
⊢ r a b → r b c → r a c

Tactic:
_root_.trans

Premises used: trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Symm r
⊢ r a b → r b a

Tactic:
symm

Premises used: symm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Asymm r
⊢ r a b → ¬r b a

Tactic:
asymm

Premises used: asymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ r a b ∨ r b a

Tactic:
Std.Total.total _ _

Premises used: Std.Total.total
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Trichotomous r
⊢ ∀ (a b : α), r a b ∨ a = b ∨ r b a

Tactic:
trichotomous

Premises used: trichotomous
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
h : Equivalence r
⊢ Symmetric r

Tactic:
fun _ _ ↦ h.symm

Premises used: Equivalence.symm, Symmetric
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
h : Equivalence r
⊢ IsTrans α r

Tactic:
⟨fun _ _ _ ↦ h.trans⟩

Premises used: IsTrans.mk, Equivalence.trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r_1 : α → α → Prop
a b c : α
β : Sort u_2
r : β → β → Prop
f : α → β
inst : IsTrans β r
⊢ IsTrans α (InvImage r f)

Tactic:
⟨fun _ _ _ ↦ trans_of r⟩

Premises used: IsTrans.mk, trans_of
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r_1 : α → α → Prop
a b c : α
β : Sort u_2
r : β → β → Prop
f : α → β
inst : Std.Irrefl r
⊢ Std.Irrefl (InvImage r f)

Tactic:
⟨fun (a : α) (h₁ : InvImage r f a a) ↦ irrefl_of r (f a) h₁⟩

Premises used: irrefl_of, Std.Irrefl.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Type u_1
inst : LE α
P : α → Prop
x : α
h : Minimal P x
⊢ P x

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Type u_1
inst : LE α
P : α → Prop
x y : α
h : Minimal P x
hy : P y
hle : y ≤ x
⊢ x ≤ y

Tactic:
h.2 hy hle

Premises used: And.right