α : 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
α : 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'
refine' ⟨h, fun ho => _⟩
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

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
α : 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
cases' lt_trichotomy a b with hab hab
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
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
have hab : Compares Ordering.lt a b := hab
no goals
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
rwa [ho.inj (h hab)]
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

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
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
cases' hab with hab hab
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
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
have hab : Compares Ordering.eq a b := hab
no goals
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
rwa [ho.inj (h hab)]
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
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
have hab : Compares Ordering.gt a b := hab
no goals
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
rwa [ho.inj (h hab)]