From 486550b79b6bc0dfe6d4d47d46ff830894823b2e Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 27 Apr 2023 15:06:17 -0600
Subject: [PATCH] Finish pairwise theorems; progress on partition theorems.

---
 Bookshelf/List/Basic.lean                   | 30 +++++----------------
 OneVariableCalculus/Real/Set/Partition.lean | 22 +++++++++++++--
 2 files changed, 27 insertions(+), 25 deletions(-)

diff --git a/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean
index 6b29285..60ae2bd 100644
--- a/Bookshelf/List/Basic.lean
+++ b/Bookshelf/List/Basic.lean
@@ -148,28 +148,6 @@ theorem zip_with_nonempty_iff_args_nonempty
     rw [has, hbs]
     simp
 
-private lemma fin_zip_with_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length}
-  : i.1 < length xs := by
-  have hi := i.2
-  simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi
-  exact hi.left
-
-private lemma fin_zip_with_imp_val_lt_length_right {i : Fin (zipWith f xs ys).length}
-  : i.1 < length ys := by
-  have hi := i.2
-  simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi
-  exact hi.right
-
-/--
-Calling `get _ i` on a zip of `xs` and `ys` is the same as applying the function
-argument to each of `get xs i` and `get ys i` directly.
--/
-theorem get_zip_with_apply_get_get {i : Fin (zipWith f xs ys).length}
-  : get (zipWith f xs ys) i = f
-      (get xs ⟨i.1, fin_zip_with_imp_val_lt_length_left⟩)
-      (get ys ⟨i.1, fin_zip_with_imp_val_lt_length_right⟩) := by
-  sorry
-
 -- ========================================
 -- Pairwise
 -- ========================================
@@ -225,6 +203,12 @@ theorem mem_pairwise_imp_length_self_ge_2 {xs : List α} (h : xs.pairwise f ≠
     | nil => rw [hx'] at h; simp at h
     | cons a' bs' => unfold length length; rw [add_assoc]; norm_num
 
+private lemma fin_zip_with_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length}
+  : i.1 < length xs := by
+  have hi := i.2
+  simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi
+  exact hi.left
+
 /--
 If `x` is a member of the pairwise'd list, there must exist two (adjacent)
 elements of the list, say `x₁` and `x₂`, such that `x = f x₁ x₂`.
@@ -286,7 +270,7 @@ theorem mem_pairwise_imp_exists {xs : List α} (h : x ∈ xs.pairwise f)
       = get ys { val := ↑i, isLt := i_lt_length_ys } := by
       conv => lhs; unfold get; simp
     rw [hx₂_offset_idx] at hx₂
-    rw [get_zip_with_apply_get_get, ← hx₁, ← hx₂] at hx
+    rw [get_zipWith, ← hx₁, ← hx₂] at hx
     exact Eq.symm hx
 
 end List
diff --git a/OneVariableCalculus/Real/Set/Partition.lean b/OneVariableCalculus/Real/Set/Partition.lean
index 16faec1..56e4ca4 100644
--- a/OneVariableCalculus/Real/Set/Partition.lean
+++ b/OneVariableCalculus/Real/Set/Partition.lean
@@ -40,12 +40,30 @@ provided it lies somewhere in closed interval `[a, b]`.
 instance : Membership ℝ Partition where
   mem (x : ℝ) (p : Partition) := p.left ≤ x ∧ x ≤ p.right
 
+/--
+Every subdivision point is `≥` the left-most point of the partition.
+-/
+theorem subdivision_point_geq_left {p : Partition} (h : x ∈ p.xs)
+  : p.left ≤ x := by
+  suffices ∀ i : Fin p.xs.length, p.left ≤ List.get p.xs i by
+    rw [List.mem_iff_exists_get] at h
+    have ⟨i, hi⟩ := h
+    rw [← hi]
+    exact this i
+  intro ⟨i, hi⟩
+  sorry
+
+/--
+Every subdivision point is `≤` the right-most point of the partition.
+-/
+theorem subdivision_point_leq_right {p : Partition} (h : x ∈ p.xs)
+  : x ≤ p.right := sorry
+
 /--
 Every subdivision point of a `Partition` is itself a member of the `Partition`.
 -/
 theorem subdivision_point_mem_partition {p : Partition} (h : x ∈ p.xs)
-  : x ∈ p := by
-  sorry
+  : x ∈ p := ⟨subdivision_point_geq_left h, subdivision_point_leq_right h⟩
 
 end Partition