internlm/Lean-Github huggingface dataset:
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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]
Proof 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))
Theorem: dirichletKernel_eq
Proof 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
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof 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)
Theorem: dirichletKernel_eq
Proof 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]
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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]
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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]
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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))]
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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
Theorem: dirichletKernel_eq
Proof 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']
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N

N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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⁻¹
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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]
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ -Int.ofNat N ≤ ↑N
Tactic:
simp
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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]
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof 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
Theorem: dirichletKernel_eq
Proof 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]
Proof 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)
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof 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
Proof state after:
no goals