diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean
index 1bd981b8111b8..7b8027fd78cf6 100644
--- a/src/data/polynomial/basic.lean
+++ b/src/data/polynomial/basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import algebra.monoid_algebra.basic
+import data.finset.sort
 
 /-!
 # Theory of univariate polynomials
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index 0cd1144cbf2ce..2c444b6b90190 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 -/
-import data.finset.sort
+import data.finset.basic
 import data.set.functor
 import data.finite.basic
 
@@ -1227,27 +1227,27 @@ s.finite_to_set.bdd_below
 
 end finset
 
-/--
-If a set `s` does not contain any elements between any pair of elements `x, z ∈ s` with `x ≤ z`
-(i.e if given `x, y, z ∈ s` such that `x ≤ y ≤ z`, then `y` is either `x` or `z`), then `s` is
-finite.
--/
-lemma set.finite_of_forall_between_eq_endpoints {α : Type*} [linear_order α] (s : set α)
-  (h : ∀ (x ∈ s) (y ∈ s) (z ∈ s), x ≤ y → y ≤ z → x = y ∨ y = z) :
-  set.finite s :=
+variables [linear_order α]
+
+/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
+is finite. -/
+lemma finite.of_forall_not_lt_lt (h : ∀ ⦃x y z : α⦄, x < y → y < z → false) :
+  finite α :=
 begin
-  by_contra hinf,
-  change s.infinite at hinf,
-  rcases hinf.exists_subset_card_eq 3 with ⟨t, hts, ht⟩,
-  let f := t.order_iso_of_fin ht,
-  let x := f 0,
-  let y := f 1,
-  let z := f 2,
-  have := h x (hts x.2) y (hts y.2) z (hts z.2)
-    (f.monotone $ by dec_trivial) (f.monotone $ by dec_trivial),
-  have key₁ : (0 : fin 3) ≠ 1 := by dec_trivial,
-  have key₂ : (1 : fin 3) ≠ 2 := by dec_trivial,
-  cases this,
-  { dsimp only [x, y] at this, exact key₁ (f.injective $ subtype.coe_injective this) },
-  { dsimp only [y, z] at this, exact key₂ (f.injective $ subtype.coe_injective this) }
+  nontriviality α,
+  rcases exists_pair_ne α with ⟨x, y, hne⟩,
+  refine @finite.of_fintype α ⟨{x, y}, λ z , _⟩,
+  simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y
 end
+
+/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite. -/
+lemma set.finite_of_forall_not_lt_lt {s : set α} (h : ∀ (x y z ∈ s), x < y → y < z → false) :
+  set.finite s :=
+@set.to_finite _ s $ finite.of_forall_not_lt_lt $ by simpa only [set_coe.forall'] using h
+
+lemma set.finite_diff_Union_Ioo (s : set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).finite :=
+set.finite_of_forall_not_lt_lt $ λ x hx y hy z hz hxy hyz, hy.2 $ mem_Union₂_of_mem hx.1 $
+  mem_Union₂_of_mem hz.1 ⟨hxy, hyz⟩
+
+lemma set.finite_diff_Union_Ioo' (s : set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).finite :=
+by simpa only [Union, supr_prod, supr_subtype] using s.finite_diff_Union_Ioo
diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean
index ae3b12da0eabf..4d7319d3a66ad 100644
--- a/src/measure_theory/constructions/borel_space.lean
+++ b/src/measure_theory/constructions/borel_space.lean
@@ -485,11 +485,7 @@ begin
   let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y,
   have huopen : is_open u := is_open_bUnion (λ x hx, is_open_bUnion (λ y hy, is_open_Ioo)),
   have humeas : measurable_set u := huopen.measurable_set,
-  have hfinite : (s \ u).finite,
-  { refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
-    by_contra' h,
-    exact hy.2 (mem_Union₂.mpr ⟨x, hx.1,
-      mem_Union₂.mpr ⟨z, hz.1, lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩⟩) },
+  have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo,
   have : u ⊆ s :=
     Union₂_subset (λ x hx, Union₂_subset (λ y hy, Ioo_subset_Icc_self.trans (h.out hx hy))),
   rw ← union_diff_cancel this,
diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index b69c07450b49a..8bd9fe374a079 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -542,12 +542,7 @@ begin
   two endpoints, which don't matter since `μ` does not have any atom). -/
   let T : s × s → set ℝ := λ p, Ioo p.1 p.2,
   let u := ⋃ (i : ↥s × ↥s), T i,
-  have hfinite : (s \ u).finite,
-  { refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
-    by_contra' h,
-    apply hy.2,
-    exact mem_Union_of_mem (⟨x, hx.1⟩, ⟨z, hz.1⟩)
-      ⟨lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩ },
+  have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo',
   obtain ⟨A, A_count, hA⟩ :
     ∃ (A : set (↥s × ↥s)), A.countable ∧ (⋃ (i ∈ A), T i) = ⋃ (i : ↥s × ↥s), T i :=
     is_open_Union_countable _ (λ p, is_open_Ioo),
@@ -584,12 +579,7 @@ begin
   two endpoints, which don't matter since `μ` does not have any atom). -/
   let T : s × s → set ℝ := λ p, Ioo p.1 p.2,
   let u := ⋃ (i : ↥s × ↥s), T i,
-  have hfinite : (s \ u).finite,
-  { refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
-    by_contra' h,
-    apply hy.2,
-    exact mem_Union_of_mem (⟨x, hx.1⟩, ⟨z, hz.1⟩)
-      ⟨lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩ },
+  have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo',
   obtain ⟨A, A_count, hA⟩ :
     ∃ (A : set (↥s × ↥s)), A.countable ∧ (⋃ (i ∈ A), T i) = ⋃ (i : ↥s × ↥s), T i :=
     is_open_Union_countable _ (λ p, is_open_Ioo),
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 7d174e19e8aff..61feee4706316 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -876,6 +876,16 @@ or_iff_not_imp_left.2 $ λ h,
   ⟨λ a ha₁, le_of_not_gt $ λ ha₂, h ⟨a, ha₁, ha₂⟩,
     λ a ha₂, le_of_not_gt $ λ ha₁, h ⟨a, ha₁, ha₂⟩⟩
 
+/-- If a linear order has no elements `x < y < z`, then it has at most two elements. -/
+lemma eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type*} [linear_order α]
+  (h : ∀ ⦃x y z : α⦄, x < y → y < z → false) (x y z : α) : x = y ∨ y = z ∨ x = z :=
+begin
+  by_contra hne, push_neg at hne,
+  cases hne.1.lt_or_lt with h₁ h₁; cases hne.2.1.lt_or_lt with h₂ h₂;
+    cases hne.2.2.lt_or_lt with h₃ h₃,
+  exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
+end
+
 namespace punit
 variables (a b : punit.{u+1})