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

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

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

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

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

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

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