-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₁ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₂ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₃ :
  cexp (HPow.hPow (β := ℕ) I 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₄ :
  cexp (-1 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₅ rw₆ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))

Tactic:
rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]

Premises used: mul_assoc, HurwitzZeta.jacobiTheta₂'', neg_one_mul, HurwitzZeta.oddKernel_def, Complex.ofReal, Complex.I_sq, Complex.I