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

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

State before:
α : Type
inst✝ : Order α
x y : α
⊢ (compare x y).isLE = true ∨ (compare y x).isLE = true
Tactic:
match cmp : compare x y with
| .lt | .eq => simp [Ordering.isLE, cmp]
| .gt =>
  apply Or.inr
  rw [←symm, cmp]
  decide
State after:
no goals

State before:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.eq
⊢ Ordering.eq.isLE = true ∨ (compare y x).isLE = true
Tactic:
simp [Ordering.isLE, cmp]
State after:
no goals

State before:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true ∨ (compare y x).isLE = true
Tactic:
apply Or.inr
State after:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ (compare y x).isLE = true

State before:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ (compare y x).isLE = true
Tactic:
rw [←symm, cmp]
State after:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap.isLE = true

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