Theorem: Order.le_of_lt (QuickSortInLean/Order.lean)

State before:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ x ≤ y
Tactic:
show (compare x y).isLE
State after:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ (compare x y).isLE = true

State before:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ (compare x y).isLE = true
Tactic:
simp [ltOfOrd] at h
State after:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
⊢ (compare x y).isLE = true

State before:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
⊢ (compare x y).isLE = true
Tactic:
match cmp : compare x y with
| .lt => decide
| .eq | .gt =>
  rw [cmp] at h
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : Order α
x y : α
h cmp : compare x y = Ordering.lt
⊢ Ordering.lt.isLE = true
Tactic:
decide
State after:
no goals

State before:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
rw [cmp] at h
State after:
α : Type
inst✝ : Order α
x y : α
h : Ordering.gt = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true

State before:
α : Type
inst✝ : Order α
x y : α
h : Ordering.gt = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
contradiction
State after:
no goals