-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Restatement of `jacobiTheta₂'_add_left'`: the function `jacobiTheta₂''` is 1-periodic in `z`. -/
lemma jacobiTheta₂''_add_left (z τ : ℂ) : jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ

Proof state:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) / (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' / (2 * ↑π * I) + z * J)

Tactic:
simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]

Result:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
        (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) +
          (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) /
      (2 * ↑π * I) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I)) / (2 * ↑π * I)

Proof state:
z τ J : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * J) / (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * J)

Tactic:
generalize jacobiTheta₂' (z * τ) τ = J'

Result:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) / (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' / (2 * ↑π * I) + z * J)

Proof state:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))

Tactic:
congrm (cexp ?_ * ?_) <;> ring

Result:
no goals

Proof state:
z τ : ℂ
⊢ jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ

Tactic:
simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']

Result:
z τ : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * jacobiTheta₂ (z * τ) τ) /
          (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) +
          cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * jacobiTheta₂ (z * τ) τ)

Proof state:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))

Tactic:
rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
  ← Complex.exp_add]

Result:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))

Proof state:
z τ : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * jacobiTheta₂ (z * τ) τ) /
          (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) +
          cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * jacobiTheta₂ (z * τ) τ)

Tactic:
generalize jacobiTheta₂ (z * τ) τ = J

Result:
z τ J : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * J) / (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * J)