dist_dirichletApprox_le

lemma dist_dirichletApprox_le    {r : ℝ} (hr : r ∈ Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊) {x : ℝ} (hx : x ∈ Icc (-π) π) :    dist (dirichletApprox n x) ({y : ℝ | |y| ∈ Ico r 1}.indicator k x) ≤ 12 * niceKernel r x := by  have rpos : 0 < r := hr.1  have hn1 : n < r⁻¹ + 1 := by    rw [hn]    exact Nat.ceil_lt_add_one (by simpa using rpos.le)  have hn2 : n ≤ 2 * r⁻¹ := by    have : 1 ≤ r⁻¹ := (one_le_inv₀ hr.1).2 hr.2.le    apply hn1.le.trans (by linarith)  rcases lt_or_ge (|x|) r with h'x | h'x  · rw [indicator_of_notMem]; swap    · simp [h'x]    simp only [dist_zero_right]    apply norm_dirichletApprox_le.trans    rw [niceKernel_eq_inv' _ h'x.le]; swap    · simp only [hr.1, true_and]      linarith [Real.pi_gt_d2, hr.2]    linarith  have hexpx : exp (I * x) ≠ 1 := by    simp only [ne_eq, exp_I_mul_eq_one_iff_of_lt_of_lt x (by linarith [hx.1, Real.pi_pos])      (by linarith [hx.2, Real.pi_pos])]    intro h    simp only [h, abs_zero] at h'x    linarith  have hnzero : n ≠ 0 := by    intro h    simp only [h, eq_comm, Nat.ceil_eq_zero, inv_nonpos] at hn    linarith  rw [dirichletApprox_eq_add_dirichletApproxAux hexpx hnzero, dist_eq_norm, add_sub_right_comm]  apply (norm_add_le _ _).trans  have A : ‖(1 - exp (I * x))⁻¹ - {y | |y| ∈ Ico r 1}.indicator k x‖ ≤ 2 * niceKernel r x := by    apply norm_sub_indicator_k h'x _ rpos hr.2    simpa only [Real.norm_eq_abs, abs_le] using! hx  have B : ‖dirichletApproxAux n x‖ ≤ 10 * niceKernel r x := by    apply norm_dirichletApproxAux_le hexpx h'x _ _ hr.1 hr.2    · simp [abs_le, hx.1, hx.2]    · rw [hn]      apply Nat.le_ceil  linarith