[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases xy : x ≤ y
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
[PROOFSTEP]
cases not_or_of_not xy yx (total_of _ _ _)
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases xy : x ≤ y
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
[PROOFSTEP]
cases not_or_of_not xy yx (total_of _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares (swap o) a b ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap lt) a b ↔ Compares lt b a
[PROOFSTEP]
exact Iff.rfl
[GOAL]
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap eq) a b ↔ Compares eq b a
[PROOFSTEP]
exact eq_comm
[GOAL]
case gt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap gt) a b ↔ Compares gt b a
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
o o' : Ordering
⊢ swap o = o' ↔ o = swap o'
[PROOFSTEP]
rw [← swap_inj, swap_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares eq a b
h : eq = lt
⊢ a < b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
h : gt = lt
⊢ a < b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares eq a b
x✝ : b ≤ a
h : eq = lt
⊢ False
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
x✝ : b ≤ a
h : gt = lt
⊢ False
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares lt a b
h : lt = eq
⊢ a = b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
h : gt = eq
⊢ a = b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
⊢ Compares o a b ↔ Compares o a' b'
[PROOFSTEP]
refine' ⟨h, fun ho => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
⊢ Compares o a b
[PROOFSTEP]
cases' lt_trichotomy a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a < b
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.lt a b := hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : a < b
hab : Compares lt a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a = b ∨ b < a
⊢ Compares o a b
[PROOFSTEP]
cases' hab with hab hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a = b
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.eq a b := hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : a = b
hab : Compares eq a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : b < a
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.gt a b := hab
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : b < a
hab : Compares gt a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
α : Type u_1
β : Type u_2
o₁ o₂ : Ordering
⊢ swap (orElse o₁ o₂) = orElse (swap o₁) (swap o₂)
[PROOFSTEP]
cases o₁
[GOAL]
case lt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse lt o₂) = orElse (swap lt) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
case eq
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse eq o₂) = orElse (swap eq) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
case gt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse gt o₂) = orElse (swap gt) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
o₁ o₂ : Ordering
⊢ orElse o₁ o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₁
[GOAL]
case lt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse lt o₂ = lt ↔ lt = lt ∨ lt = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case eq
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse eq o₂ = lt ↔ eq = lt ∨ eq = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case gt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse gt o₂ = lt ↔ gt = lt ∨ gt = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case lt.lt
α : Type u_1
β : Type u_2
⊢ orElse lt lt = lt ↔ lt = lt ∨ lt = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt lt = lt ↔ lt = lt ∨ lt = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case lt.eq
α : Type u_1
β : Type u_2
⊢ orElse lt eq = lt ↔ lt = lt ∨ lt = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt eq = lt ↔ lt = lt ∨ lt = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case lt.gt
α : Type u_1
β : Type u_2
⊢ orElse lt gt = lt ↔ lt = lt ∨ lt = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt gt = lt ↔ lt = lt ∨ lt = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
case eq.lt
α : Type u_1
β : Type u_2
⊢ orElse eq lt = lt ↔ eq = lt ∨ eq = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq lt = lt ↔ eq = lt ∨ eq = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case eq.eq
α : Type u_1
β : Type u_2
⊢ orElse eq eq = lt ↔ eq = lt ∨ eq = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq eq = lt ↔ eq = lt ∨ eq = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case eq.gt
α : Type u_1
β : Type u_2
⊢ orElse eq gt = lt ↔ eq = lt ∨ eq = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq gt = lt ↔ eq = lt ∨ eq = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
case gt.lt
α : Type u_1
β : Type u_2
⊢ orElse gt lt = lt ↔ gt = lt ∨ gt = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt lt = lt ↔ gt = lt ∨ gt = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case gt.eq
α : Type u_1
β : Type u_2
⊢ orElse gt eq = lt ↔ gt = lt ∨ gt = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt eq = lt ↔ gt = lt ∨ gt = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case gt.gt
α : Type u_1
β : Type u_2
⊢ orElse gt gt = lt ↔ gt = lt ∨ gt = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt gt = lt ↔ gt = lt ∨ gt = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares o (↑toDual a) (↑toDual b) ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares lt (↑toDual a) (↑toDual b) ↔ Compares lt b a
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares eq (↑toDual a) (↑toDual b) ↔ Compares eq b a
case gt α : Type u_1 β : Type u_2 inst✝ : LT α a b : α ⊢ Compares gt (↑toDual a) (↑toDual b) ↔ Compares gt b a
[PROOFSTEP]
exacts [Iff.rfl, eq_comm, Iff.rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
o : Ordering
⊢ Compares o (↑ofDual a) (↑ofDual b) ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares lt (↑ofDual a) (↑ofDual b) ↔ Compares lt b a
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares eq (↑ofDual a) (↑ofDual b) ↔ Compares eq b a
case gt α : Type u_1 β : Type u_2 inst✝ : LT α a b : αᵒᵈ ⊢ Compares gt (↑ofDual a) (↑ofDual b) ↔ Compares gt b a
[PROOFSTEP]
exacts [Iff.rfl, eq_comm, Iff.rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ Compares (cmp a b) a b
[PROOFSTEP]
obtain h | h | h := lt_trichotomy a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (cmp a b) = cmp b a
[PROOFSTEP]
unfold cmp cmpUsing
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h₂ : b < a
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h₂ : b < a
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : ¬b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
h₂ : b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ False
[PROOFSTEP]
exact lt_asymm h h₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ cmp x x = eq
[PROOFSTEP]
rw [cmp_eq_eq_iff]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
[PROOFSTEP]
rwa [← cmp_swap x', ← cmp_swap, swap_inj]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'
[PROOFSTEP]
rwa [← cmp_swap y', ← cmp_swap, swap_inj]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'
[PROOFSTEP]
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'
[PROOFSTEP]
rw [← not_lt, ← not_lt]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
[PROOFSTEP]
apply not_congr
[GOAL]
case h
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'
[PROOFSTEP]
apply lt_iff_lt_of_cmp_eq_cmp
[GOAL]
case h.h
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
[PROOFSTEP]
rwa [cmp_eq_cmp_symm]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'
[PROOFSTEP]
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h, le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]
