-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem TransCmp.compareOfLessAndEq
    [LT α] [DecidableRel (LT.lt (α := α))] [DecidableEq α]
    (lt_irrefl : ∀ x : α, ¬x < x)
    (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
    (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) :
    TransCmp (α := α) (compareOfLessAndEq · ·)

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
this : OrientedCmp fun x1 x2 => compareOfLessAndEq x1 x2
x y z : α
yx : ¬y < x
zy : ¬z < y
⊢ ¬z < x

Tactic:
intro zx

Result:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
this : OrientedCmp fun x1 x2 => compareOfLessAndEq x1 x2
x y z : α
yx : ¬y < x
zy : ¬z < y
zx : z < x
⊢ False

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
⊢ OrientedCmp fun x1 x2 => compareOfLessAndEq x1 x2

Tactic:
refine { symm := fun x y => ?_ }

Result:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
⊢ (compareOfLessAndEq x y).swap = compareOfLessAndEq y x

Proof state:
case isFalse.isFalse.isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
xy : ¬x < y
ne : ¬x = y
yx : ¬y < x
⊢ Ordering.gt.swap = if y = x then Ordering.eq else Ordering.gt

Tactic:
cases ne (lt_antisymm xy yx)

Result:
no goals

Proof state:
case isTrue.hnc
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
xy : x < y
⊢ ¬y = x

Tactic:
rintro rfl

Result:
case isTrue.hnc
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
y : α
xy : y < y
⊢ False

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
⊢ (if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt).swap =
    if y < x then Ordering.lt else if y = x then Ordering.eq else Ordering.gt

Tactic:
split <;> [rename_i xy; split <;> [subst y; rename_i xy ne]]

Result:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
xy : x < y
⊢ Ordering.lt.swap = if y < x then Ordering.lt else if y = x then Ordering.eq else Ordering.gt

case isFalse.isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x : α
h✝ : ¬x < x
⊢ Ordering.eq.swap = if x < x then Ordering.lt else if x = x then Ordering.eq else Ordering.gt

case isFalse.isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
xy : ¬x < y
ne : ¬x = y
⊢ Ordering.gt.swap = if y < x then Ordering.lt else if y = x then Ordering.eq else Ordering.gt

Proof state:
case isFalse.isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x : α
h✝ : ¬x < x
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue.hnc
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
x y : α
xy : x < y
⊢ ¬y < x

Tactic:
exact fun yx => lt_irrefl _ (lt_trans xy yx)

Result:
no goals

Proof state:
case isTrue.hnc
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
y : α
xy : y < y
⊢ False

Tactic:
exact lt_irrefl _ xy

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
lt_irrefl : ∀ (x : α), ¬x < x
lt_trans : ∀ {x y z : α}, x < y → y < z → x < z
lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y
this : OrientedCmp fun x1 x2 => compareOfLessAndEq x1 x2
x y z : α
yx : ¬y < x
zy : ¬z < y
zx : z < x
xy : ¬x < y
⊢ False

Tactic:
exact zy (lt_antisymm yx xy ▸ zx)

Result:
no goals