RS.IPart.fromPoints_strictMono

The points of fromPoints s are exactly s. -/ lemma points_fromPoints {a b : ℝ} (s : Finset ℝ) (ha : a ∈ s) (hb : b ∈ s) (h_sub : (s : Set ℝ) ⊆ Set.Icc a b) : (fromPoints (a:=a) (b:=b) s ha hb h_sub).points = s := by classical -- replicate the local defs used in fromPoints, so we can reuse them let l : List ℝ := s.sort (· ≤ ·)

have hs_nonempty : s.Nonempty := ⟨a, ha⟩ have hlpos : 0 < l.length := by simpa [l, Finset.length_sort] using (Finset.card_pos.mpr hs_nonempty)

let n : ℕ := l.length.pred have hn : n.succ = l.length := Nat.succ_pred_eq_of_pos hlpos have hn' : n + 1 = l.length := by simpa [Nat.succ_eq_add_one] using hn

ext y constructor · intro hy -- unfold points and fromPoints enough to get "y is some l.get ..." -- (we keep [l,n] in simp so it doesn't explode) have hy' : y ∈ (Finset.univ : Finset (Fin (n + 1))).image (fun i => l.get ⟨i.1, by -- this is exactly the bound proof used in fromPoints simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩) := by -- this is what points is, after unfolding fromPoints simpa [IPartition.points, fromPoints, l, n] using hy

rcases Finset.mem_image.mp hy' with ⟨i, hiuniv, rfl⟩
-- Now show this list element is in s, since l = s.sort ...
have : l.get ⟨i.1, by
    simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩ ∈ l :=
  List.get_mem l _
-- Convert list-membership in l to finset-membership in s using mem_sort
exact (Finset.mem_sort (s := s) (r := (· ≤ ·))).1 (by simpa [l] using this)

· intro hy -- y ∈ s → y ∈ l have hyL : y ∈ l := (Finset.mem_sort (s := s) (r := (· ≤ ·))).2 (by simpa using hy) -- pick an index j with l.get j = y rcases List.mem_iff_get.mp hyL with ⟨j, rfl⟩

-- We need to show l.get j is in the image of x over Fin (n+1).
-- Use i := cast j into Fin (n+1).
let i : Fin (n + 1) := Fin.cast hn'.symm j

-- Unfold points/fromPoints and provide witness i
have : l.get j ∈ (Finset.univ : Finset (Fin (n + 1))).image (fun i =>
  l.get ⟨i.1, by
    simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩) := by
  refine Finset.mem_image.mpr ?_
  refine ⟨i, Finset.mem_univ _, ?_⟩
  -- Compare the Fin indices used in the two gets
  -- j : Fin l.length, while the RHS uses ⟨i.1, _⟩ : Fin l.length.
  -- Show they are equal by Fin.ext (only vals matter).
  have hjlen : (⟨i.1, by
      -- i.2 : i.1 < n+1, rewrite via hn' to get i.1 < l.length
      simpa [hn', i] using i.2⟩ : Fin l.length) = j := by
    apply Fin.ext
    rfl
  -- Then the gets are equal
  simpa [hjlen]

-- now translate back to the original goal
simpa [IPartition.points, fromPoints, l, n] using this

/- The union of two partitions P and Q is the partition constructed from the union of their point sets. -/ def union {a b : ℝ} (P Q : IPartition a b) : IPartition a b := fromPoints (P.points ∪ Q.points) (by exact Finset.mem_union_left _ ( Finset.mem_image.mpr ⟨ 0, Finset.mem_univ _, P.left ⟩ )) (by exact Finset.mem_union.mpr ( Or.inl <| Finset.mem_image.mpr ⟨ Fin.last _, Finset.mem_univ _, P.right ⟩ )) (by -- Since $P$ and $Q$ are partitions of $[a, b]$, their points are within $[a, b]$. have hP : ∀ y ∈ P.points, y ∈ Set.Icc a b := by intro y hy; obtain ⟨ i, hi, rfl ⟩ := Finset.mem_image.mp hy; exact ⟨ by linarith [ P.monotone ( show 0 ≤ i from Nat.zero_le _ ), P.left ], by linarith [ P.monotone ( show i ≤ Fin.last P.n from Fin.le_last _ ), P.right ] ⟩ ; have hQ : ∀ y ∈ Q.points, y ∈ Set.Icc a b := by rintro y hy; obtain ⟨ i, _, rfl ⟩ := Finset.mem_image.mp hy; exact ⟨ by linarith [ Q.left, Q.right, Q.monotone ( show 0 ≤ i from Nat.zero_le _ ) ], by linarith [ Q.left, Q.right, Q.monotone ( show i ≤ Fin.last Q.n from Fin.le_last _ ) ] ⟩ ; grind)

lemma union_points {a b : ℝ} (P Q : IPartition a b) : (union P Q).points = P.points ∪ Q.points := by -- unfolds to fromPoints on the finset union simp [union, points_fromPoints]

/- The union of two partitions refines both. -/

lemma union_refines_left {a b : ℝ} (P Q : IPartition a b) : IsRefinement (union P Q) P := by -- goal: P.points ⊆ (union P Q).points -- i.e. P.points ⊆ P.points ∪ Q.points simpa [IsRefinement, union_points] using (Finset.subset_union_left : P.points ⊆ P.points ∪ Q.points)

lemma union_refines_right {a b : ℝ} (P Q : IPartition a b) : IsRefinement (union P Q) Q := by simpa [IsRefinement, union_points] using (Finset.subset_union_right : Q.points ⊆ P.points ∪ Q.points)

/- The points of a partition constructed from a set of points are strictly increasing.