Theorem: dirichletKernel_eq (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
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 in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
      rw [dirichletKernel, mul_sum]
      congr
      ext n
      simp [sub_mul, ← exp_add, ← exp_add]
      congr <;>
      . ring_nf
        congr 1
        rw [mul_assoc, mul_assoc]
        congr
        rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
        norm_cast
        exact Real.pi_pos.ne.symm
    _ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat 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]
      symm
      rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
      congr
      symm
      rw [sub_eq_zero]
      conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
      congr
      . ext 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]
      . ext n
        congr
        simp [add_assoc, sub_eq_add_neg]
        congr
        norm_num
      . rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
        norm_cast
      all_goals simp
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
⊢ dirichletKernel N x = dirichletKernel' N x

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
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]
      congr
      rw [mul_assoc, ← mul_add]
      ring
    _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by
      congr
    _ = 1 := by
      rw [← exp_add]
      ring_nf
      exact exp_zero
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = dirichletKernel' N x

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = dirichletKernel' N x
Tactic:
rw [dirichletKernel']
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ dirichletKernel N x = cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Tactic:
apply mul_left_cancel₀ h'
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) *
      (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) *
      (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)) + cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
rw [this, mul_add, sub_eq_add_neg]
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) + -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))) +
      (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) + -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))) +
      (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
congr
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))

case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))

case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
. 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
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
. rw [mul_div]
  apply eq_div_of_mul_eq
  . contrapose! h
    rwa [sub_eq_zero, eq_comm] at h
  ring_nf
  rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]
  congr 2 <;> ring
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (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)
Tactic:
calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
  _ = ∑ n in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
    rw [dirichletKernel, mul_sum]
    congr
    ext n
    simp [sub_mul, ← exp_add, ← exp_add]
    congr <;>
    . ring_nf
      congr 1
      rw [mul_assoc, mul_assoc]
      congr
      rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
      norm_cast
      exact Real.pi_pos.ne.symm
  _ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat 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]
    symm
    rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
    congr
    symm
    rw [sub_eq_zero]
    conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
    congr
    . ext 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]
    . ext n
      congr
      simp [add_assoc, sub_eq_add_neg]
      congr
      norm_num
    . rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
      norm_cast
    all_goals simp
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, (cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x))
Tactic:
rw [dirichletKernel, mul_sum]
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ i ∈ Icc (-Int.ofNat N) ↑N, (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier i) ↑x =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, (cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x))

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ i ∈ Icc (-Int.ofNat N) ↑N, (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier i) ↑x =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, (cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x))
Tactic:
congr
State after:
case e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun i => (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier i) ↑x) = fun n =>
    cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x)

State before:
case e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun i => (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier i) ↑x) = fun n =>
    cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x)
Tactic:
ext n
State after:
case e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier n) ↑x =
    cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x)

State before:
case e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (fourier n) ↑x =
    cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x)
Tactic:
simp [sub_mul, ← exp_add, ← exp_add]
State after:
case e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ cexp (2⁻¹ * I * ↑x + 2 * ↑Real.pi * I * ↑n * ↑x / (2 * ↑Real.pi)) -
      cexp (-1 / 2 * I * ↑x + 2 * ↑Real.pi * I * ↑n * ↑x / (2 * ↑Real.pi)) =
    cexp ((↑n + 2⁻¹) * I * ↑x) - cexp (↑n * I * ↑x - 2⁻¹ * I * ↑x)

State before:
case e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ cexp (2⁻¹ * I * ↑x + 2 * ↑Real.pi * I * ↑n * ↑x / (2 * ↑Real.pi)) -
      cexp (-1 / 2 * I * ↑x + 2 * ↑Real.pi * I * ↑n * ↑x / (2 * ↑Real.pi)) =
    cexp ((↑n + 2⁻¹) * I * ↑x) - cexp (↑n * I * ↑x - 2⁻¹ * I * ↑x)
Tactic:
congr <;>
. ring_nf
  congr 1
  rw [mul_assoc, mul_assoc]
  congr
  rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
  norm_cast
  exact Real.pi_pos.ne.symm
State after:
no goals

State before:
case e_f.h.e_a.e_z
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ -1 / 2 * I * ↑x + 2 * ↑Real.pi * I * ↑n * ↑x / (2 * ↑Real.pi) = ↑n * I * ↑x - 2⁻¹ * I * ↑x
Tactic:
ring_nf
State after:
case e_f.h.e_a.e_z
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * (-1 / 2) + I * ↑x * ↑Real.pi * ↑n * (↑Real.pi)⁻¹ = I * ↑x * (-1 / 2) + I * ↑x * ↑n

State before:
case e_f.h.e_a.e_z
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * (-1 / 2) + I * ↑x * ↑Real.pi * ↑n * (↑Real.pi)⁻¹ = I * ↑x * (-1 / 2) + I * ↑x * ↑n
Tactic:
congr 1
State after:
case e_f.h.e_a.e_z.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * ↑Real.pi * ↑n * (↑Real.pi)⁻¹ = I * ↑x * ↑n

State before:
case e_f.h.e_a.e_z.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * ↑Real.pi * ↑n * (↑Real.pi)⁻¹ = I * ↑x * ↑n
Tactic:
rw [mul_assoc, mul_assoc]
State after:
case e_f.h.e_a.e_z.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * (↑Real.pi * (↑n * (↑Real.pi)⁻¹)) = I * ↑x * ↑n

State before:
case e_f.h.e_a.e_z.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ I * ↑x * (↑Real.pi * (↑n * (↑Real.pi)⁻¹)) = I * ↑x * ↑n
Tactic:
congr
State after:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑Real.pi * (↑n * (↑Real.pi)⁻¹) = ↑n

State before:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑Real.pi * (↑n * (↑Real.pi)⁻¹) = ↑n
Tactic:
rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
State after:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑Real.pi ≠ 0

State before:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑Real.pi ≠ 0
Tactic:
norm_cast
State after:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ¬Real.pi = 0

State before:
case e_f.h.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ¬Real.pi = 0
Tactic:
exact Real.pi_pos.ne.symm
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, (cexp ((↑n + 1 / 2) * I * ↑x) - cexp ((↑n - 1 / 2) * I * ↑x)) =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, cexp ((↑n + 1 / 2) * I * ↑x) -
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, cexp ((↑n - 1 / 2) * I * ↑x)
Tactic:
rw [sum_sub_distrib]
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, cexp ((↑n + 1 / 2) * I * ↑x) -
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, cexp ((↑n - 1 / 2) * I * ↑x) =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
Tactic:
rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x)) =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x)) =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
symm
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x))

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x))

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ 0 + (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)) =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x))

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ 0 + (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)) =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
        ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) +
      (cexp ((↑↑N + 1 / 2) * I * ↑x) - cexp ((↑(-Int.ofNat N) - 1 / 2) * I * ↑x))

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
congr
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ 0 =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
      ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ 0 =
    ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
      ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
symm
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
      ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) =
    0

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) -
      ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x) =
    0

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
rw [sub_eq_zero]
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N) ↑N, cexp ((↑x_1 + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N + 1) (↑N + 1), cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ∑ x_1 ∈ Ico (-Int.ofNat N + 1) (↑N + 1), cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x) =
    ∑ x_1 ∈ Ioc (-Int.ofNat N) ↑N, cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
congr
State after:
case e_a.e_s
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ Ico (-Int.ofNat N + 1) (↑N + 1) = Ioc (-Int.ofNat N) ↑N

case e_a.e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun x_1 => cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x)) = fun x_1 => cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a.e_s
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ Ico (-Int.ofNat N + 1) (↑N + 1) = Ioc (-Int.ofNat N) ↑N

case e_a.e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun x_1 => cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x)) = fun x_1 => cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
. ext 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]
State after:
case e_a.e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun x_1 => cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x)) = fun x_1 => cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a.e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun x_1 => cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x)) = fun x_1 => cexp ((↑x_1 - 1 / 2) * I * ↑x)

case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
. ext n
  congr
  simp [add_assoc, sub_eq_add_neg]
  congr
  norm_num
State after:
case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
. rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
  norm_cast
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
all_goals simp
State after:
no goals

State before:
case e_a.e_s
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ Ico (-Int.ofNat N + 1) (↑N + 1) = Ioc (-Int.ofNat N) ↑N
Tactic:
ext n
State after:
case e_a.e_s.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ n ∈ Ico (-Int.ofNat N + 1) (↑N + 1) ↔ n ∈ Ioc (-Int.ofNat N) ↑N

State before:
case e_a.e_s.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ n ∈ Ico (-Int.ofNat N + 1) (↑N + 1) ↔ n ∈ Ioc (-Int.ofNat N) ↑N
Tactic:
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]
State after:
no goals

State before:
case e_a.e_f
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ (fun x_1 => cexp ((↑(x_1 + -1) + 1 / 2) * I * ↑x)) = fun x_1 => cexp ((↑x_1 - 1 / 2) * I * ↑x)
Tactic:
ext n
State after:
case e_a.e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ cexp ((↑(n + -1) + 1 / 2) * I * ↑x) = cexp ((↑n - 1 / 2) * I * ↑x)

State before:
case e_a.e_f.h
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ cexp ((↑(n + -1) + 1 / 2) * I * ↑x) = cexp ((↑n - 1 / 2) * I * ↑x)
Tactic:
congr
State after:
case e_a.e_f.h.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑(n + -1) + 1 / 2 = ↑n - 1 / 2

State before:
case e_a.e_f.h.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ ↑(n + -1) + 1 / 2 = ↑n - 1 / 2
Tactic:
simp [add_assoc, sub_eq_add_neg]
State after:
case e_a.e_f.h.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ -1 + 2⁻¹ = -2⁻¹

State before:
case e_a.e_f.h.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
n : ℤ
⊢ -1 + 2⁻¹ = -2⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -(↑N + 1 / 2) = ↑(-Int.ofNat N) - 1 / 2
Tactic:
rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
State after:
case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -↑N + -(1 / 2) = -↑↑N + -(1 / 2)

State before:
case e_a.e_a.e_z.e_a.e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -↑N + -(1 / 2) = -↑↑N + -(1 / 2)
Tactic:
norm_cast
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
simp
State after:
no goals

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
⊢ cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
Tactic:
contrapose! h
State after:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) = 0
⊢ cexp (I * ↑x) = 1

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Tactic:
rw [sub_eq_zero] at h
State after:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (I * ↑x) = 1

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (I * ↑x) = 1
Tactic:
calc cexp (I * ↑x)
  _ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by
    rw [← exp_add]
    congr
    rw [mul_assoc, ← mul_add]
    ring
  _ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by
    congr
  _ = 1 := by
    rw [← exp_add]
    ring_nf
    exact exp_zero
State after:
no goals

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (I * ↑x) = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x)
Tactic:
rw [← exp_add]
State after:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (I * ↑x) = cexp (1 / 2 * I * ↑x + 1 / 2 * I * ↑x)

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (I * ↑x) = cexp (1 / 2 * I * ↑x + 1 / 2 * I * ↑x)
Tactic:
congr
State after:
case e_z
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ I * ↑x = 1 / 2 * I * ↑x + 1 / 2 * I * ↑x

State before:
case e_z
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ I * ↑x = 1 / 2 * I * ↑x + 1 / 2 * I * ↑x
Tactic:
rw [mul_assoc, ← mul_add]
State after:
case e_z
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ I * ↑x = 1 / 2 * (I * ↑x + I * ↑x)

State before:
case e_z
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ I * ↑x = 1 / 2 * (I * ↑x + I * ↑x)
Tactic:
ring
State after:
no goals

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x)
Tactic:
congr
State after:
no goals

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) = 1
Tactic:
rw [← exp_add]
State after:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x + -1 / 2 * I * ↑x) = 1

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x + -1 / 2 * I * ↑x) = 1
Tactic:
ring_nf
State after:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp 0 = 1

State before:
N : ℕ
x : ℝ
this :
  (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)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp 0 = 1
Tactic:
exact exp_zero
State after:
no goals

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))
Tactic:
rw [mul_div]
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))
Tactic:
apply eq_div_of_mul_eq
State after:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)

State before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Tactic:
. contrapose! h
  rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Tactic:
ring_nf
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) * cexp (-(I * ↑x)) =
    cexp (I * ↑x * (1 / 2)) * cexp (↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2)) * cexp (↑N * I * ↑x)

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) * cexp (-(I * ↑x)) =
    cexp (I * ↑x * (1 / 2)) * cexp (↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2)) * cexp (↑N * I * ↑x)
Tactic:
rw [← exp_add, ← exp_add, ← exp_add]
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2) + -(I * ↑x)) =
    cexp (I * ↑x * (1 / 2) + ↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2) + ↑N * I * ↑x)

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2) + -(I * ↑x)) =
    cexp (I * ↑x * (1 / 2) + ↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2) + ↑N * I * ↑x)
Tactic:
congr 2 <;> ring
State after:
no goals

State before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0
Tactic:
contrapose! h
State after:
case e_a.hc
N : ℕ
x : ℝ
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (-I * ↑x) = 0
⊢ cexp (I * ↑x) = 1

State before:
case e_a.hc
N : ℕ
x : ℝ
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (-I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Tactic:
rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
State after:
no goals

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
rw [mul_div]
State after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))

State before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Tactic:
apply eq_div_of_mul_eq
State after:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)

State before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Tactic:
. contrapose! h
  rwa [sub_eq_zero, eq_comm] at h
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Tactic:
ring_nf
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) + cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) * cexp (I * ↑x) =
    cexp (I * ↑x * (1 / 2)) * cexp (-(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2)) * cexp (-(↑N * I * ↑x))

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) + cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) * cexp (I * ↑x) =
    cexp (I * ↑x * (1 / 2)) * cexp (-(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2)) * cexp (-(↑N * I * ↑x))
Tactic:
rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]
State after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2) + I * ↑x) - cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) =
    cexp (I * ↑x * (1 / 2) + -(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2) + -(↑N * I * ↑x))

State before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2) + I * ↑x) - cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) =
    cexp (I * ↑x * (1 / 2) + -(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2) + -(↑N * I * ↑x))
Tactic:
congr 2 <;> ring
State after:
no goals

State before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0
Tactic:
contrapose! h
State after:
case e_a.hc
N : ℕ
x : ℝ
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (I * ↑x) = 0
⊢ cexp (I * ↑x) = 1

State before:
case e_a.hc
N : ℕ
x : ℝ
this :
  (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)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Tactic:
rwa [sub_eq_zero, eq_comm] at h
State after:
no goals