awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rwa : 0 < (↑x : ℂ).re
⊢ 0 < (I * (↑x : ℂ)).im
have rwa₁ : ℂ
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ HasSum (fun (x_1 : ℤ) ↦ (↑(((↑x_1 : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑x_1 : ℝ) + a) 2 * x)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
have h2 : HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
  (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ HasSum (fun (x_1 : ℤ) ↦ (↑(((↑x_1 : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑x_1 : ℝ) + a) 2 * x)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
have refine : ∀ (n : ℤ),
  (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
    (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw : (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
  ((↑n : ℂ) + (↑a : ℂ)) *
    cexp
      (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
Tactic: rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
    mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
have push_cast : ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
  ((↑n : ℂ) + (↑a : ℂ)) *
    cexp
      (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
have simp : ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
  ((↑n : ℂ) + (↑a : ℂ)) *
    cexp
      ((-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I) *
        (↑x : ℂ))
Tactic: simp only [← mul_assoc, ← add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        ((-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
            (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I) *
          (↑x : ℂ))
have congrm : -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
  -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
    (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I
Tactic: congrm _ * cexp (?_ * x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
    -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I
have simp : -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
  -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
    (2 * (↑π : ℂ) * (↑n : ℂ) * (↑a : ℂ) * -1 + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * -1)
Tactic: simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have h : -2 * (↑π : ℂ) ≠ 0
Tactic: have h : -2 * (π : ℂ) ≠ (0 : ℂ) := by
    simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero,
      OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have rw : HasSum
  (fun (n : ℤ) ↦
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
  (jacobiTheta₂' (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ)))
Tactic: rw [sinKernel_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
⊢ 0 < (I * (↑t : ℂ)).im
have rwa : 0 < (↑t : ℂ).re
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂' (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ)))
have refine : ∀ (n : ℤ),
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    jacobiTheta₂'_term n (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ))
Tactic: refine ((hasSum_jacobiTheta₂'_term a
    (by rwa [I_mul_im, ofReal_re])).div_const _).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    jacobiTheta₂'_term n (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ))
have rw : -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
Tactic: rw [jacobiTheta₂'_term, jacobiTheta₂_term, ofReal_exp, mul_assoc (-I * n), ← Complex.exp_add,
    eq_div_iff h, ofReal_mul, ofReal_mul, ofReal_pow, ofReal_neg, ofReal_intCast,
    mul_comm _ (-2 * π : ℂ), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
have refine_1 : -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) = 2 * (↑π : ℂ) * I * (↑n : ℂ)
Tactic: congrm ?_ * cexp (?_ + ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
refine_1 : -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) = 2 * (↑π : ℂ) * I * (↑n : ℂ)
⊢ -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
have refine_2 : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ)
Tactic: congrm ?_ * cexp (?_ + ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
refine_1 : -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) = 2 * (↑π : ℂ) * I * (↑n : ℂ)
refine_2 : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ)
⊢ -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
have refine_3 : -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ) =
  (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))
Tactic: congrm ?_ * cexp (?_ + ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℕ) ↦
      HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t))
    (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t)
have rw : HasSum
  (fun (x : ℕ) ↦
    (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
      ℂ))
  (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
Tactic: rw [← hasSum_ofReal]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
            rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
        ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have this : HasSum
  (fun (n : ℕ) ↦
    -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
  ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
    -I * (↑0 : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
Tactic: have := (hasSum_int_sinKernel a ht).nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      -I * (↑0 : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
            rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
        ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have this₁ : HasSum
  (fun (n : ℕ) ↦
    -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
  (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
Tactic: simp only [Int.cast_zero, zero_mul, mul_zero, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
            rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
        ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have refine : ∀ (n : ℕ),
  (↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) :
      ℂ) =
    -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ)
Tactic: refine this.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
⊢ (↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) :
      ℂ) =
    -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ)
have simp_rw : HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
      ((cexp (-(↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) - cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)) * I / 2) *
    (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
  (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
      -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
    (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)
Tactic: simp_rw [Int.cast_neg, neg_sq, mul_neg, ofReal_mul, Int.cast_natCast, ofReal_natCast,
      ofReal_ofNat, ← add_mul, ofReal_sin, Complex.sin]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) - cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)) * I / 2) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)
have push_cast : HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
      ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) *
    cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
  (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
      -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
    cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))
have e_a : HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
    ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) =
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
    -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
      ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
      -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))
have e_a : I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) -
    I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) =
  I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) -
    I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
Tactic: rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul,
    neg_mul, neg_mul, neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul,
    ← sub_eq_neg_add, mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
⊢ I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) =
    I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
have e_a : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
Tactic: congr 3