-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Compare.lean
theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
[Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a'

Proof state:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : ¬a < a'
h : (if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Tactic:
next =>
  split at h
  next => assumption
  next => simp at h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h : compareOfLessAndEq a a' = Ordering.eq
⊢ a = a'

Tactic:
unfold compareOfLessAndEq at h

Result:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h : (if a < a' then Ordering.lt else if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : ¬a = a'
h : Ordering.gt = Ordering.eq
⊢ a = a'

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h : (if a < a' then Ordering.lt else if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Tactic:
split at h

Result:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : a < a'
h : Ordering.lt = Ordering.eq
⊢ a = a'

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : ¬a < a'
h : (if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : a < a'
h : Ordering.lt = Ordering.eq
⊢ a = a'

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : a = a'
h : Ordering.eq = Ordering.eq
⊢ a = a'

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : ¬a < a'
h : (if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Tactic:
split at h

Result:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : a = a'
h : Ordering.eq = Ordering.eq
⊢ a = a'

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : ¬a = a'
h : Ordering.gt = Ordering.eq
⊢ a = a'

Proof state:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : a < a'
h : Ordering.lt = Ordering.eq
⊢ a = a'

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : ¬a < a'
h : (if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Tactic:
next =>
  simp at h

Result:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝ : ¬a < a'
h : (if a = a' then Ordering.eq else Ordering.gt) = Ordering.eq
⊢ a = a'

Proof state:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : ¬a = a'
h : Ordering.gt = Ordering.eq
⊢ a = a'

Tactic:
next => simp at h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : a = a'
h : Ordering.eq = Ordering.eq
⊢ a = a'

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : ¬a = a'
h : Ordering.gt = Ordering.eq
⊢ a = a'

Tactic:
next => assumption

Result:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a a' : α
inst✝ : Decidable (a < a')
h✝¹ : ¬a < a'
h✝ : ¬a = a'
h : Ordering.gt = Ordering.eq
⊢ a = a'