dirichletKernel_eq

lemma dirichletKernel_eq {x : ℝ} (h : cexp (I * x) ≠ 1) :    dirichletKernel N x = dirichletKernel' N x := by  have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x      = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by    calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x      _ = ∑ n ∈ Icc (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by        rw [dirichletKernel, mul_sum]        congr 1 with n        simp [sub_mul, ← exp_add, ← exp_add]        congr 2 <;>        · ring_nf          congr 1          rw [mul_assoc, mul_assoc]          congr          rw_mod_cast [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel₀, one_mul]          exact Real.pi_pos.ne.symm      _ = ∑ n ∈ Icc (-(N : ℤ)) N, cexp ((n + 1 / 2) * I * ↑x)          - ∑ n ∈ Icc (-(N : ℤ)) N, cexp ((n - 1 / 2) * I * ↑x) := by        rw [sum_sub_distrib]      _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by        rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm,          ← zero_add (cexp ((N + 1 / 2) * I * ↑x) - cexp (-(N + 1 / 2) * I * ↑x))]        · congr 2          · rw [sub_eq_zero]            conv => lhs; rw [← Int.add_sub_cancel (-(N : ℤ)) 1, sub_eq_add_neg,              ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']            congr 2 with n            · rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right,              ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc]              simp            · simp only [Int.reduceNeg, Int.cast_add, Int.cast_neg, Int.cast_one, one_div, add_assoc,                sub_eq_add_neg]              norm_num          · rw [neg_add_rev, add_comm, Int.cast_neg, sub_eq_add_neg]            norm_cast        all_goals simp  have h' : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) ≠ 0 := by    contrapose! h    rw [sub_eq_zero] at h    calc cexp (I * ↑x)      _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by        rw [← exp_add, mul_assoc, ← mul_add]        ring_nf      _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by congr 2      _ = 1 := by        rw [← exp_add]        ring_nf        exact exp_zero  rw [dirichletKernel']  apply mul_left_cancel₀ h'  rw [this, mul_add, sub_eq_add_neg]  congr  · rw [mul_div]    apply eq_div_of_mul_eq    · contrapose! h      rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h    ring_nf    rw [← exp_add, ← exp_add, ← exp_add]    congr 2 <;> ring  · rw [mul_div]    apply eq_div_of_mul_eq (sub_ne_zero_of_ne h.symm)    ring_nf    rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]    congr 2 <;> ring