refactor(data/set/finite): reduce imports (#18245)

* Add `eq_or_eq_or_eq_of_forall_not_lt_lt`, `finite.of_forall_not_lt_lt`, `set.finite_of_forall_not_lt_lt` (replacing `set.finite_of_forall_between_eq_endpoints`), and `set.finite_of_forall_not_lt_lt'`.
* Import `data.finset.basic` instead of `data.finset.sort` in `data.set.finite`.
* Forward-ported in leanprover-community/mathlib4#1738

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

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

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,

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),

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})