exact
  match lt_trichotomy (x - a) 0, lt_trichotomy (y - b) 0 with
  | Or.inl xaNeg,           Or.inl ybNeg           => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inl (And.intro xaNeg' ybNeg')
  | Or.inl xaNeg,           Or.inr (Or.inl ybZero) => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybZero' := le_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaNeg' ybZero')
  | Or.inl xaNeg,           Or.inr (Or.inr ybPos)  => by nlinarith
  | Or.inr (Or.inl xaZero), Or.inl ybNeg           => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inl (And.intro xaZero' ybNeg')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inl ybZero) => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybZero' := le_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaZero' ybZero')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inr ybPos)  => by
    have xaZero' := ge_of_eq xaZero
    simp at xaZero'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inr (And.intro xaZero' ybPos')
  | Or.inr (Or.inr xaPos),  Or.inl ybNeg           => by nlinarith
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inl ybZero) => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inr (And.intro xaPos' ybZero')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inr ybPos)  => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inr (And.intro xaPos' ybPos')
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≥ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
no goals