Refactor: reduce imports of Data.Set.Finite (#1738)

Partial forward-port of leanprover-community/mathlib#18245

Mathlib/Data/Set/Finite.lean

@@ -8,7 +8,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Data.Finset.Sort
+import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Set.Functor
 import Mathlib.Data.Finite.Basic
 
@@ -1550,19 +1550,30 @@ protected theorem bddBelow [SemilatticeInf α] [Nonempty α] (s : Finset α) : B
 
 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.
--/
-theorem Set.finite_of_forall_between_eq_endpoints {α : Type _} [LinearOrder α] (s : Set α)
-    (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x ≤ y → y ≤ z → x = y ∨ y = z) : Set.Finite s := by
-  by_contra hinf
-  replace hinf : s.Infinite := hinf
-  rcases hinf.exists_subset_card_eq 3 with ⟨t, hts, ht⟩
-  let f := t.orderIsoOfFin 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 decide) (f.monotone <| by decide)
-  simp at this
-#align set.finite_of_forall_between_eq_endpoints Set.finite_of_forall_between_eq_endpoints
+variable [LinearOrder α] {s : Set α}
+
+/-- 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 α := by
+  -- porting note: todo: use `nontriviality α` instead of the first 2 lines
+  cases subsingleton_or_nontrivial α
+  · exact Finite.of_subsingleton
+  · rcases exists_pair_ne α with ⟨x, y, hne⟩
+    refine' @Finite.of_fintype α ⟨{x, y}, fun z => _⟩
+    simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y
+#align finite.of_forall_not_lt_lt Finite.of_forall_not_lt_lt
+
+/-- 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 (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) :
+    Set.Finite s :=
+  @Set.toFinite _ s <| Finite.of_forall_not_lt_lt $ by simpa only [SetCoe.forall'] using h
+#align set.finite_of_forall_not_lt_lt Set.finite_of_forall_not_lt_lt
+
+lemma Set.finite_diff_unionᵢ_Ioo (s : Set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).Finite :=
+  Set.finite_of_forall_not_lt_lt fun _x hx _y hy _z hz hxy hyz => hy.2 <| mem_unionᵢ₂_of_mem hx.1 <|
+    mem_unionᵢ₂_of_mem hz.1 ⟨hxy, hyz⟩
+#align set.finite_diff_Union_Ioo Set.finite_diff_unionᵢ_Ioo
+
+lemma Set.finite_diff_unionᵢ_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite := by
+  simpa only [unionᵢ, supᵢ_prod, supᵢ_subtype] using s.finite_diff_unionᵢ_Ioo
+#align set.finite_diff_Union_Ioo' Set.finite_diff_unionᵢ_Ioo'

Mathlib/Order/Basic.lean

@@ -1233,6 +1233,16 @@ theorem dense_or_discrete [LinearOrder α] (a₁ a₂ : α) :
      fun a ha₂ ↦ le_of_not_gt fun ha₁ ↦ h ⟨a, ha₁, ha₂⟩⟩
 #align dense_or_discrete dense_or_discrete
 
+/-- 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 [LinearOrder α]
+    (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) (x y z : α) : x = y ∨ y = z ∨ x = z := by
+  by_contra hne
+  simp only [not_or, ← Ne.def] 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₁]
+#align eq_or_eq_or_eq_of_forall_not_lt_lt eq_or_eq_or_eq_of_forall_not_lt_lt
+
 namespace PUnit
 
 variable (a b : PUnit.{u + 1})