awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
have rw : -(↑π : ℂ) * I * (HPow.hPow (β := ℕ) (↑a : ℂ) 2 * -1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) =
  -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) * (I * (↑x : ℂ))
Tactic: rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have h4 : -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
  -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
Tactic: have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
    rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
      jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₁ : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₁ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₂ : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₁ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₂ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₃ : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₁ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₂ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₃ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₄ : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)))) *
    jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₁ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₂ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₃ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₄ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₅ : 1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
have inr : ∀ (a : ℝ),
  evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (1 / 2) * cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
Tactic: induction a using QuotientAddGroup.induction_on with | H a =>
  rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
  have h1 : I * ↑(1 / x) = -1 / (I * x) := by
    push_cast
    rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
  have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
  have h2 : a * I * x / (I * x) = a := by
    rw [div_eq_iff hx']
    ring
  have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
    rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
  have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
    rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
    ring
  rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t)
have rw : HasSum (fun (x : ℤ) ↦ (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑x : ℝ) + a) 2 * t)) : ℂ))
  (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) * jacobiTheta₂ ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ)))
Tactic: rw [← hasSum_ofReal, evenKernel_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
      jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))
have rw : cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
  cexp
    (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) +
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑t : ℂ)) +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))))
Tactic: rw [jacobiTheta₂_term, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun (x : ℤ) ↦ (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑x : ℝ) + a) 2 * t)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) *
      jacobiTheta₂ ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ)))
have this : ∀ (n : ℤ),
  cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
      jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))
Tactic: have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) *
      jacobiTheta₂_term n (a * I * t) (I * t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    grind [I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℤ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
have rw : HasSum
  (fun (n : ℤ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
  (jacobiTheta₂ (↑a : ℂ) (I * (↑t : ℂ)))
Tactic: rw [cosKernel_def a t]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))
have rw : cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
Tactic: rw [jacobiTheta₂_term, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
have ring_nf : cexp ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 - (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
  cexp
    ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℤ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂ (↑a : ℂ) (I * (↑t : ℂ)))
have this : ∀ (n : ℤ),
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))
Tactic: have (n : ℤ) : cexp (2 * π * I * a * n) * cexp (-(π * n ^ 2 * t)) =
      jacobiTheta₂_term n a (I * ↑t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    ring_nf
    simp [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
            (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
        1
      else 0)
have haveI : ∀ (this : (a : Prop) → Decidable a),
  HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
            (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
        1
      else 0)
Tactic: haveI := Classical.propDecidable
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
            (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
        1
      else 0)
have simp_rw : HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
  (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if ∃ (n : ℤ), (↑n : ℝ) = a then 1 else 0)
Tactic: simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if ∃ (n : ℤ), (↑n : ℝ) = a then 1 else 0)
have pos : ∀ (h : ∃ (n : ℤ), (↑n : ℝ) = a),
  HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
pos :
  ∀ (h : ∃ (n : ℤ), (↑n : ℝ) = a),
    HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
      (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if ∃ (n : ℤ), (↑n : ℝ) = a then 1 else 0)
have neg : ∀ (h : ¬∃ (n : ℤ), (↑n : ℝ) = a),
  HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) = a
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
have pos : ∀ (k : ℤ),
  HasSum
    (fun (n : ℤ) ↦
      if HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ) = 0 then 0
      else rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ)) 2 * t))
    (evenKernel (↑(↑k : ℝ) : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: a, h