Dirichlet_Hilbert_diff

lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-π) π) :    ‖dirichletKernel' N (x) - (exp (I * (-N * x)) * k x + conj (exp (I * (-N * x)) * k x))‖ ≤ π := by  rw [← Dirichlet_Hilbert_eq]  by_cases! h : 1 - cexp (I * ↑x) = 0  · rw [sub_eq_zero] at h    rw [dirichletKernel'_eq_zero h.symm]    simp [pi_pos.le]  conv => pattern (dirichletKernel' N x); rw [← (one_mul (dirichletKernel' N x))]  rw [← sub_mul]  norm_cast  rw [← min_sub_sub_left]  simp only [_root_.sub_sub_cancel, sub_zero]  rw [dirichletKernel', mul_add]  calc ‖  (min |x| 1) * (exp (I * N * x) / (1 - exp (-I * x)))        + (min |x| 1) * (exp (-I * N * x) / (1 - exp (I * x)))‖    _ ≤   ‖(min |x| 1) * (exp (I * N * x) / (1 - exp (-I * x)))‖        + ‖(min |x| 1) * (exp (-I * N * x) / (1 - exp (I * x)))‖ := by      apply norm_add_le    _ ≤ |x| * (1 / ‖1 - exp (I * x)‖) + |x| * (1 / ‖1 - exp (I * x)‖) := by      simp only [neg_mul, norm_mul, norm_real, norm_div]      rw [Real.norm_of_nonneg (by simp)]      gcongr      · apply min_le_left      · rw [mul_assoc I, mul_comm I]        norm_cast        rw [norm_exp_ofReal_mul_I]      · rw [← norm_conj, map_sub, map_one, ←exp_conj, ← neg_mul, map_mul, conj_I, conj_ofReal]      · apply min_le_left      · /-Duplicate from above:        TODO: how to remove duplicate goals? -/        rw [mul_assoc I, mul_comm I, ← neg_mul]        norm_cast        rw [norm_exp_ofReal_mul_I]    _ = 2 * (|x| / ‖1 - exp (I * x)‖) := by ring    _ ≤ 2 * (π / 2) := by      gcongr 2 * ?_      rw [div_le_iff₀' (by rwa [norm_pos_iff]), ← div_le_iff₀ (by linarith [pi_pos]),        div_div_eq_mul_div, mul_div_assoc, mul_comm]      apply lower_secant_bound' (by rfl)      have : |x| ≤ π := by        rwa [abs_le]      linarith    _ = π := by ring