RS.IPart.points_fromPoints

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