Chebyshev.psi_diff_le_weighted

@[blueprint  "cheby-psi-diff"  (title := "Upper bounding a difference of $\\psi$ by a weighted sum of $T$")  (statement := /-- For any $x > 0$, one has $\psi(x) - \psi(x/6) \leq U(x)$. -/)  (proof := /-- Use Lemma \ref{cheby-T-E}, Lemma \ref{cheby-E-val}, and Lemma \ref{cheby-E-1}. -/)  (latexEnv := "proposition")  (discussion := 838)]theorem psi_diff_le_weighted (x : ℝ) (hx : x > 0) : ψ x - ψ (x / 6) ≤ U x := by  unfold U psi  rw [T.weighted_eq_sum, ← Ioc_eq_Icc]  have subset : Ioc 0 ⌊x / 6⌋₊ ⊆ Ioc 0 ⌊x⌋₊ := by    apply Ioc_subset_Ioc_right    gcongr    exact div_le_self hx.le (by norm_num)  rw [← sum_sdiff_eq_sub subset, ← sum_sdiff subset]  refine le_add_of_le_of_nonneg (sum_le_sum fun n hn ↦ ?_) (sum_nonneg fun n hn ↦ mul_nonneg vonMangoldt_nonneg ?_)  · rw [E_nu_eq_one, mul_one]    simp_all only [gt_iff_lt, Finset.mem_sdiff, Finset.mem_Ioc, not_and, not_le, Set.mem_Ico]    refine ⟨one_le_div (by simp; grind)|>.mpr <| Nat.le_floor_iff hx.le |>.mp hn.1.2, ?_⟩    have := hn.2 hn.1.1    apply div_lt_iff₀ (by simp; grind)|>.mpr    rw [Nat.floor_lt <| div_nonneg (by linarith) (by linarith)] at this    have := div_lt_iff₀ (by linarith)|>.mp this    rwa [mul_comm] at this  · exact E_nu_bound _ (div_nonneg hx.le (by simp))|>.1