awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
⊢ IncompRel rᶜ = AntisymmRel r

Tactic:
simp [← antisymmRel_compl, compl]

Premises used: Compl.compl, antisymmRel_compl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ IncompRel rᶜ a b ↔ AntisymmRel r a b

Tactic:
simp
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
⊢ IncompRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) = IncompRel r

Tactic:
antisymmRel_swap rᶜ

Premises used: Compl.compl, IncompRel, AntisymmRel, antisymmRel_swap
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ IncompRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ IncompRel r a b

Tactic:
antisymmRel_swap_apply rᶜ

Premises used: Compl.compl, antisymmRel_swap_apply, IncompRel, AntisymmRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
⊢ IncompRel r a a

Tactic:
AntisymmRel.refl rᶜ a

Premises used: Compl.compl, IncompRel, AntisymmRel, AntisymmRel.refl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
⊢ IncompRel r a a

Tactic:
.refl ..

Premises used: IncompRel.refl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ IncompRel r a b → IncompRel r b a

Tactic:
And.symm

Premises used: IncompRel, And.symm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ IncompRel r a b ↔ IncompRel r b a

Tactic:
comm

Premises used: comm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : IncompRel r a b
⊢ ¬AntisymmRel r a b

Tactic:
fun h' ↦ h.1 h'.1

Premises used: And.left, Not
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : AntisymmRel r a b
⊢ ¬IncompRel r a b

Tactic:
fun h' ↦ h'.1 h.1

Premises used: And.left, Not
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬SymmGen r a b ↔ IncompRel r a b

Tactic:
simp [Relation.SymmGen, IncompRel]

Premises used: IncompRel, Relation.SymmGen
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬CompRel r a b ↔ IncompRel r a b

Tactic:
not_symmGen_iff

Premises used: CompRel, not_symmGen_iff
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
rw : ¬¬SymmGen r a b ↔ SymmGen r a b
rw₁ rw₂ : SymmGen r a b ↔ SymmGen r a b
⊢ ¬IncompRel r a b ↔ SymmGen r a b

Tactic:
rw [← not_symmGen_iff, not_not]

Premises used: Classical.not_not, not_symmGen_iff
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ ¬IncompRel r a b ↔ CompRel r a b

Tactic:
not_incompRel_iff_symmGen

Premises used: CompRel, not_incompRel_iff_symmGen
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Total r
a b : α
rw : SymmGen r a b
⊢ ¬IncompRel r a b

Tactic:
rw [not_incompRel_iff_symmGen]

Premises used: not_incompRel_iff_symmGen
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ SymmGen r a b

Tactic:
symmGen_of_total a b

Premises used: Relation.symmGen_of_total
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ SymmGen r a b

Tactic:
exact symmGen_of_total a b

Premises used: Relation.symmGen_of_total
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
h : IncompRel r a a
⊢ False

Tactic:
h.1 <| refl_of r a

Premises used: refl_of, And.left
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
h : IncompRel r a a
⊢ False

Tactic:
exact h.1 <| refl_of r a

Premises used: refl_of, And.left
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : LE α
h : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬a ≤ b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : LE α
h : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬b ≤ a

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : LE α
h : a ≤ b
⊢ ¬IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
fun h' ↦ h'.not_le h

Premises used: IncompRel.not_le, Not
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬a < b

Tactic:
mt le_of_lt h.not_le

Premises used: le_of_lt, mt, IncompRel.not_le
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ ¬b < a

Tactic:
mt le_of_lt h.not_ge

Premises used: le_of_lt, mt, IncompRel.not_ge
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : a < b
⊢ ¬IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
fun h' ↦ h'.not_lt h

Premises used: IncompRel.not_lt, Not
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
rw : ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
⊢ ¬b ≤ a ↔ a < b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
rw [lt_iff_le_not_ge, IncompRel]

Premises used: lt_iff_le_not_ge, IncompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₂ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₃ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₄ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₅ : a ≤ b → ¬b ≤ a → b ≤ a → False
mpr₆ : ¬a ≤ b → ¬b ≤ a → b ≤ a → False
mp₅ : ¬b ≤ a → a ≤ b → ¬a ≤ b → False
mp₆ : ¬b ≤ a → a ≤ b → ¬¬b ≤ a → False
mpr₇ : a ≤ b → ¬b ≤ a → b ≤ a → False
mpr₈ : ¬a ≤ b → ¬b ≤ a → b ≤ a → False
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a

Tactic:
tauto
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
inst : Preorder α
a b : α
simp_rw :
  a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a < b ∨ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
simp_rw [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₈ inl₉ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₆ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₇ inr₈ inr₉ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁₀ inl₁₁ inl₁₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁₀ inr₁₁ inr₁₂ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁₃ inl₁₄ inl₁₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁₃ inr₁₄ inr₁₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁₆ inl₁₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁₆ inr₁₇ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
tauto
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
⟨fun h ↦ h₁.not_le (h.trans h₂.ge), fun h ↦ h₁.not_ge (h₂.le.trans h)⟩

Premises used: AntisymmRel.le, AntisymmRel.ge, IncompRel.not_le, IncompRel, IncompRel.not_ge, And.intro, LE.le.trans
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
(h₂.symm.trans_antisymmRel h₁.symm).symm

Premises used: IncompRel.trans_antisymmRel, AntisymmRel.symm, IncompRel.symm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c

Tactic:
h.incompRel_congr AntisymmRel.rfl

Premises used: AntisymmRel.incompRel_congr, AntisymmRel.rfl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ↔ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
AntisymmRel.rfl.incompRel_congr h

Premises used: AntisymmRel.incompRel_congr, AntisymmRel.rfl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a < b ∨ a = b ∨ b < a ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
simpa using lt_or_antisymmRel_or_gt_or_incompRel a b

Premises used: lt_or_antisymmRel_or_gt_or_incompRel
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
pos : ∀ (xy : x ≤ y), (cmpLE x y).swap = cmpLE y x
neg : ∀ (xy : ¬x ≤ y), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases xy : x ≤ y
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : x ≤ y
pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
neg : ∀ (yx : ¬y ≤ x), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases yx : y ≤ x
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
neg : ∀ (yx : ¬y ≤ x), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases yx : y ≤ x
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
simp [cmpLE, *, Ordering.swap]

Premises used: cmpLE, Ordering.swap
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
simp [cmpLE, *, Ordering.swap]

Premises used: cmpLE, Ordering.swap
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
simp [cmpLE, *, Ordering.swap]

Premises used: cmpLE, Ordering.swap
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
neg : False
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
simp [cmpLE, *, Ordering.swap]

Premises used: cmpLE, Ordering.swap
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Premises used: not_or_intro, total_of
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
pos : ∀ (xy : x ≤ y), cmpLE x y = cmp x y
neg : ∀ (xy : ¬x ≤ y), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y

Tactic:
by_cases xy : x ≤ y
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : x ≤ y
pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
neg : ∀ (yx : ¬y ≤ x), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y

Tactic:
by_cases yx : y ≤ x
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
pos : ∀ (yx : y ≤ x), cmpLE x y = cmp x y
neg : ∀ (yx : ¬y ≤ x), cmpLE x y = cmp x y
⊢ cmpLE x y = cmp x y

Tactic:
by_cases yx : y ≤ x
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Premises used: lt_iff_le_not_ge, cmpUsing, cmp, cmpLE
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Premises used: lt_iff_le_not_ge, cmpUsing, cmp, cmpLE
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Premises used: lt_iff_le_not_ge, cmpUsing, cmp, cmpLE
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
neg : False
⊢ cmpLE x y = cmp x y

Tactic:
simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]

Premises used: lt_iff_le_not_ge, cmpUsing, cmp, cmpLE
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
inst_3 : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Premises used: not_or_intro, total_of
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt : Ordering.lt.swap.Compares a b ↔ Ordering.lt.Compares b a
eq : Ordering.eq.swap.Compares a b ↔ Ordering.eq.Compares b a
gt : Ordering.gt.swap.Compares a b ↔ Ordering.gt.Compares b a
⊢ o.swap.Compares a b ↔ o.Compares b a

Tactic:
cases o
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

Tactic:
eq_comm

Premises used: eq_comm, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

Tactic:
exact eq_comm

Premises used: eq_comm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Compare
Goal:
o o' : Ordering
rw : o.swap.swap = o'.swap ↔ o = o'.swap
rw₁ rw₂ : o = o'.swap ↔ o = o'.swap
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
rw [← swap_inj, swap_swap]

Premises used: Ordering.swap_swap, Ordering.swap_inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
a b : α
h_1 : eq.Compares a b
h : eq = lt
⊢ a < b

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
a b : α
h_1 : gt.Compares a b
h : gt = lt
⊢ a < b

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
x x_1 : α
h_1 : eq.Compares x x_1
h_2 : x_1 ≤ x
h : eq = lt
⊢ False

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
x x_1 : α
h_1 : gt.Compares x x_1
h_2 : x_1 ≤ x
h : gt = lt
⊢ False

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
a b : α
h_1 : lt.Compares a b
h : lt = eq
⊢ a = b

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
a b : α
h_1 : gt.Compares a b
h : gt = eq
⊢ a = b

Tactic:
injection h
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
o : Ordering
a b : α
h : o.Compares a b
⊢ o = gt ↔ b < a

Tactic:
swap_eq_iff_eq_swap.symm.trans h.swap.eq_lt

Premises used: Ordering.swap_eq_iff_eq_swap, Ordering.Compares.eq_lt, Ordering.Compares.swap, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
o : Ordering
a b : α
h : o.Compares a b
⊢ o ≠ gt ↔ a ≤ b

Tactic:
(not_congr swap_eq_iff_eq_swap.symm).trans h.swap.ne_lt

Premises used: Ordering.swap_eq_iff_eq_swap, Ordering.Compares.swap, Iff.trans, Ordering.Compares.ne_lt, Iff.symm, not_congr
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
⟨h, fun ho => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
refine : ∀ (ho : o.Compares a' b'), o.Compares a b
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
refine ⟨h, fun ho => ?_⟩
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
inl : ∀ (hab : a < b), o.Compares a b
inr : ∀ (hab : a = b), o.Compares a b
inr₁ : ∀ (hab : b < a), o.Compares a b
⊢ o.Compares a b

Tactic:
rcases lt_trichotomy a b with hab | hab | hab

Premises used: lt_trichotomy
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ lt.Compares a b

Tactic:
have hab : Compares Ordering.lt a b := hab
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab_1 : a < b
hab : lt.Compares a b
inl inl₁ inl₂ inl₃ : lt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Premises used: Ordering.Compares.inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ eq.Compares a b

Tactic:
have hab : Compares Ordering.eq a b := hab
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab_1 : a = b
hab : eq.Compares a b
inr inr₁ inr₂ inr₃ : eq.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Premises used: Ordering.Compares.inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ gt.Compares a b

Tactic:
have hab : Compares Ordering.gt a b := hab
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab_1 : b < a
hab : gt.Compares a b
inr inr₁ inr₂ inr₃ : gt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Premises used: Ordering.Compares.inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
o : Ordering
lt :
  Ordering.lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.lt.Compares b a
eq :
  Ordering.eq.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.eq.Compares b a
gt :
  Ordering.gt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔
    Ordering.gt.Compares b a
⊢ o.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ o.Compares b a

Tactic:
cases o
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ lt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ eq.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ eq.Compares b a

Tactic:
eq_comm

Premises used: eq_comm, Ordering.Compares, OrderDual
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ gt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ gt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ lt.Compares (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ lt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Premises used: Iff.rfl, eq_comm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
o : Ordering
lt :
  Ordering.lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.lt.Compares b a
eq :
  Ordering.eq.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.eq.Compares b a
gt :
  Ordering.gt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔
    Ordering.gt.Compares b a
⊢ o.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ o.Compares b a

Tactic:
cases o
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
⊢ lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ lt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares