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

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

State before:
α : Type
inst✝ : Order α
x : α
⊢ (compare x x).isLE = true
Tactic:
simp [cmp_eq_of_eq]
State after:
α : Type
inst✝ : Order α
x : α
⊢ Ordering.eq.isLE = true

State before:
α : Type
inst✝ : Order α
x : α
⊢ Ordering.eq.isLE = true
Tactic:
decide
State after:
no goals