ZetaAppendix.tendsto_sine_series_of_not_int

lemma tendsto_sine_series_of_not_int {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :    Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) / (n + 1 : ℝ))      atTop (𝓝 (Real.pi * (1 / 2 - Int.fract x))) := by  have hfract_ne : Int.fract x ≠ 0 := by    intro h0    rcases (Int.fract_eq_zero_iff.mp h0) with ⟨k, hk⟩    exact hx ⟨k, hk.symm⟩  have hfract_pos : 0 < Int.fract x :=    lt_of_le_of_ne (Int.fract_nonneg x) (Ne.symm hfract_ne)  have hunit := tendsto_sine_series_unit_interval hfract_pos (Int.fract_lt_one x)  refine hunit.congr' ?_  filter_upwards with N  apply Finset.sum_congr rfl  intro n _hn  rw [← sin_two_pi_mul_nat_fract x n]