-- Mathlib/Order/Compare.lean
theorem compares_iff_of_compares_impl [LinearOrder α] [Preorder β] {a b : α} {a' b' : β}
    (h : ∀ {o}, Compares o a b → Compares o a' b') (o) : Compares o a b ↔ Compares o a' b'

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.lt a b := hab

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ o.Compares a b

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : b < a
hab : gt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a = b
hab : eq.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
refine ⟨h, fun ho => ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
⊢ o.Compares a b

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ o.Compares a b

Tactic:
rwa [ho.inj (h hab)]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.eq a b := hab

Result:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a = b
hab : eq.Compares a b
⊢ o.Compares a b

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.gt a b := hab

Result:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : b < a
hab : gt.Compares a b
⊢ o.Compares a b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
⊢ o.Compares a b

Tactic:
rcases lt_trichotomy a b with hab | hab | hab

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b