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

State before:
α : Type
inst✝ : Order α
x : α
⊢ compare x x = Ordering.eq
Tactic:
match cmp : compare x x with
| .eq => rfl
| .lt =>
  have h₁ : (compare x x).swap = .gt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .lt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
| .gt =>
  have h₁ : (compare x x).swap = .lt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .gt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
State after:
no goals

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.eq
⊢ Ordering.eq = Ordering.eq
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
have h₁ : (compare x x).swap = .gt := by rw [cmp]; decide
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ Ordering.lt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ Ordering.lt = Ordering.eq
Tactic:
have h₂ : (compare x x).swap = .lt := by rw [symm]; assumption
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
rw [h₂] at h₁
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : Ordering.lt = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : Ordering.lt = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ (compare x x).swap = Ordering.gt
Tactic:
rw [cmp]
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ Ordering.lt.swap = Ordering.gt

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

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ (compare x x).swap = Ordering.lt
Tactic:
rw [symm]
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ compare x x = Ordering.lt

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ compare x x = Ordering.lt
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
have h₁ : (compare x x).swap = .lt := by rw [cmp]; decide
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ Ordering.gt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ Ordering.gt = Ordering.eq
Tactic:
have h₂ : (compare x x).swap = .gt := by rw [symm]; assumption
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
rw [h₂] at h₁
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : Ordering.gt = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : Ordering.gt = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ (compare x x).swap = Ordering.lt
Tactic:
rw [cmp]
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt

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

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ (compare x x).swap = Ordering.gt
Tactic:
rw [symm]
State after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ compare x x = Ordering.gt

State before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ compare x x = Ordering.gt
Tactic:
assumption
State after:
no goals