-- 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:
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

Tactic:
rw [if_neg ‹_›, if_pos rfl]

Result:
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

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_trans zx xy)

Result:
no goals

Proof state:
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

Tactic:
rw [if_neg, if_neg]

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 = Ordering.gt

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

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

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
⊢ TransCmp fun x1 x2 => compareOfLessAndEq x1 x2

Tactic:
refine { this with le_trans := fun {x y z} yx zy => ?_ }

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 : compareOfLessAndEq x y ≠ Ordering.gt
zy : compareOfLessAndEq y z ≠ Ordering.gt
⊢ compareOfLessAndEq x z ≠ Ordering.gt

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 : α
⊢ (compareOfLessAndEq x y).swap = compareOfLessAndEq y x

Tactic:
simp [compareOfLessAndEq]

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 : α
⊢ (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

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 : compareOfLessAndEq x y ≠ Ordering.gt
zy : compareOfLessAndEq y z ≠ Ordering.gt
⊢ compareOfLessAndEq x z ≠ Ordering.gt

Tactic:
rw [Ne, this.cmp_eq_gt, compareOfLessAndEq_eq_lt] at yx zy ⊢

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
⊢ ¬z < x

Proof state:
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

Tactic:
split <;> [rfl; rename_i yx]

Result:
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

Proof state:
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 = Ordering.gt

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

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:
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
x y : α
xy : x < y
⊢ ¬y = x

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

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
⊢ False

Tactic:
if xy : x < y then exact zy (lt_trans zx xy)
else exact zy (lt_antisymm yx xy ▸ zx)

Result:
no goals