RS.IPart.exists_refinement_mesh_le

lemma exists_refinement_mesh_le {a b : ℝ} (hab : a < b) (P : RS.IPart.IPartition a b)    {δ : ℝ} (hδ : 0 < δ) :    ∃ Q, RS.IPart.IsRefinement Q P ∧ Q.mesh ≤ δ := by  -- Choose `n` such that `(b-a)/(n+1) ≤ δ`.  obtain ⟨n, hn⟩ : ∃ n : ℕ, (b - a) / (n + 1) ≤ δ := by    refine ⟨⌊(b - a) / δ⌋₊, ?_⟩    -- your original proof:    rw [div_le_iff₀] <;> nlinarith [Nat.lt_floor_add_one ((b - a) / δ), mul_div_cancel₀ (b - a) hδ.ne']  -- Let `U` be the uniform partition of size `n`.  set U : IPart.IPartition a b := IPart.uniformPartition n hab  -- Let `Q = union P U`.  set Q : IPart.IPartition a b := RS.IPart.union P U  refine ⟨Q, ?_, ?_⟩  · exact RS.IPart.union_refines_left P U  · -- Q.mesh ≤ U.mesh ≤ δ    have hQU : Q.mesh ≤ U.mesh := by      -- IMPORTANT: `mesh_le_of_refinement` takes ONE argument: the refinement proof.      -- Here Q refines U.      simpa [Q] using (mesh_le_of_refinement (P := U) (R := Q) (RS.IPart.union_refines_right P U))    calc      Q.mesh ≤ U.mesh := hQU      _ = (b - a) / (n + 1) := by            -- rewrite the mesh of the uniform partition            simpa [U] using (RS.IPart.mesh_uniformPartition (a := a) (b := b) n hab)      _ ≤ δ := hn