BrunTitchmarsh.abs_rem_le

theorem abs_rem_le {d : ℕ} (hd : d ≠ 0) :    |rem (s := toBoundingSieve (self := primeInterSieve x y z hz)) d| ≤ 5 := by  rw [rem_eq _ _ _ hx hz _ hd]  have hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) =      (↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) : ℝ) := by    rw [Nat.cast_sub]    gcongr    rw [Nat.le_floor_iff, ← add_le_add_iff_right 1]    · rw_mod_cast [Nat.sub_add_cancel (by simp [hx])]      linarith [Nat.ceil_le_self_add_one x (le_of_lt hx)]    linarith  rw [hpush]  obtain ⟨C₁, hC₁_le, hC₁⟩ := floor_div_approx (x + y) (by linarith) d  obtain ⟨C₂, hC₂_le, hC₂⟩ := nat_div_approx (Nat.ceil x - 1) d  obtain ⟨C₃, hC₃_le, hC₃⟩ := ceil_approx (x) (by linarith)  rw [hC₁, hC₂, Nat.cast_sub, hC₃]  · ring_nf    rw [(by ring_nf : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + C₁ - C₂| = |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)|)]    have : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤        |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂| := abs_add_le _ _    have : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤        |(↑d)⁻¹| + |(↑d)⁻¹ * C₃| := abs_sub _ _    have : |C₁ - C₂| ≤ |C₁| + |C₂| := abs_sub _ _    have : |(d:ℝ)⁻¹| ≤ 1 := by      rw [abs_inv, Nat.abs_cast]      exact Nat.cast_inv_le_one _    have : |(↑d)⁻¹ * C₃| ≤ |C₃| := by      rw [inv_mul_eq_div, abs_div]      refine div_le_self (abs_nonneg _) ?_      rw [Nat.abs_cast, Nat.one_le_cast]      omega    linarith  · simp [hx]