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

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

State before:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
⊢ (compare x y).isLE = true
Tactic:
match cmp : compare x y with
| .lt | .eq => decide
| .gt =>
  simp [ltOfOrd] at h
  have : compare y x = .lt := by rw [←symm, cmp]; decide
  rw [this] at h
  contradiction
State after:
no goals

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

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

State before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
have : compare y x = .lt := by rw [←symm, cmp]; decide
State after:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
this : compare y x = Ordering.lt
⊢ Ordering.gt.isLE = true

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

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

State before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ compare y x = Ordering.lt
Tactic:
rw [←symm, cmp]
State after:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt

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