-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem LTCmp.eq_compareOfLessAndEq
    [LT α] [DecidableEq α] [BEq α] [LawfulBEq α] [BEqCmp cmp] [LTCmp cmp]
    (x y : α) [Decidable (x < y)] : cmp x y = compareOfLessAndEq x y

Proof state:
case isFalse.isFalse.eq
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.eq
⊢ Ordering.eq = Ordering.gt

Tactic:
cases h2 (BEqCmp.cmp_iff_eq.1 e)

Result:
no goals

Proof state:
case isFalse.isFalse.gt
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.gt

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse.isTrue
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : x = y
⊢ cmp x y = Ordering.eq

Tactic:
exact BEqCmp.cmp_iff_eq.2 h2

Result:
no goals

Proof state:
case isFalse.isFalse.lt
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.lt
⊢ Ordering.lt = Ordering.gt

Tactic:
cases h1 (LTCmp.cmp_iff_lt.1 e)

Result:
no goals

Proof state:
case isTrue
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : x < y
⊢ cmp x y = Ordering.lt

Tactic:
exact LTCmp.cmp_iff_lt.2 h1

Result:
no goals

Proof state:
case isFalse.isFalse
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
⊢ cmp x y = Ordering.gt

Tactic:
cases e : cmp x y

Result:
case isFalse.isFalse.lt
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.lt
⊢ Ordering.lt = Ordering.gt

case isFalse.isFalse.eq
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.eq
⊢ Ordering.eq = Ordering.gt

case isFalse.isFalse.gt
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
⊢ cmp x y = compareOfLessAndEq x y

Tactic:
simp [compareOfLessAndEq]

Result:
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
⊢ cmp x y = if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
⊢ cmp x y = if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt

Tactic:
split <;> rename_i h1 <;> [skip; split <;> rename_i h2]

Result:
case isTrue
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : x < y
⊢ cmp x y = Ordering.lt

case isFalse.isTrue
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : x = y
⊢ cmp x y = Ordering.eq

case isFalse.isFalse
α : Type u_1
cmp : α → α → Ordering
inst✝⁶ : LT α
inst✝⁵ : DecidableEq α
inst✝⁴ : BEq α
inst✝³ : LawfulBEq α
inst✝² : BEqCmp cmp
inst✝¹ : LTCmp cmp
x y : α
inst✝ : Decidable (x < y)
h1 : ¬x < y
h2 : ¬x = y
⊢ cmp x y = Ordering.gt