-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma jacobiTheta₂'_functional_equation' (z τ : ℂ) :
    jacobiTheta₂' z τ = (-2 * π) / (-I * τ) ^ (3 / 2 : ℂ) * jacobiTheta₂'' z (-1 / τ)

Proof state:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π * jacobiTheta₂'' z (-1 / τ)

Tactic:
rw [jacobiTheta₂'', div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc, ← mul_div_assoc,
  ← div_mul_eq_mul_div (-2 * π : ℂ), mul_assoc, aux1, mul_div z (-1), mul_neg_one, neg_div τ z,
  jacobiTheta₂_neg_left, jacobiTheta₂'_neg_left, neg_mul, ← mul_neg, ← mul_neg,
  mul_div, mul_neg_one, neg_div, neg_mul, neg_mul, neg_div]

Result:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Proof state:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Tactic:
congr 2

Result:
case inr.e_a.e_a.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)

Proof state:
case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-↑π * I * z ^ 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (3 / 2) * (-2 * ↑π * jacobiTheta₂'' z (-1 / τ))

Tactic:
congr 1

Result:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π * jacobiTheta₂'' z (-1 / τ)

Proof state:
z : ℂ
⊢ im 0 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
z : ℂ
⊢ jacobiTheta₂' z 0 = -2 * ↑π / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)

Tactic:
rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by norm_num), div_zero, zero_mul]

Result:
no goals

Proof state:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / 2 + 1 = 3 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case inr
z τ : ℂ
hτ : τ ≠ 0
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
have aux1 : (-2 * π : ℂ) / (2 * π * I) = I := by
  rw [div_eq_iff two_pi_I_ne_zero, mul_comm I, mul_assoc _ I I, I_mul_I, neg_mul, mul_neg,
    mul_one]

Result:
case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Proof state:
case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
rw [jacobiTheta₂'_functional_equation, ← mul_one_div _ τ, mul_right_comm _ (cexp _),
  (by rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)] :
    1 / τ = -I / (-I * τ) ^ (1 : ℂ)), div_mul_div_comm,
  ← cpow_add _ _ (mul_ne_zero (neg_ne_zero.mpr I_ne_zero) hτ), ← div_mul_eq_mul_div,
  (by norm_num : (1 / 2  + 1 : ℂ) = 3 / 2), mul_assoc (1 / _), mul_assoc (1 / _),
  ← mul_one_div (-2 * π : ℂ), mul_comm _ (1 / _), mul_assoc (1 / _)]

Result:
case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-↑π * I * z ^ 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (3 / 2) * (-2 * ↑π * jacobiTheta₂'' z (-1 / τ))

Proof state:
z : ℂ
⊢ 3 / 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.e_a.e_a.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)

Tactic:
rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]

Result:
no goals

Proof state:
z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * ↑π / (2 * ↑π * I) = I

Tactic:
rw [div_eq_iff two_pi_I_ne_zero, mul_comm I, mul_assoc _ I I, I_mul_I, neg_mul, mul_neg,
  mul_one]

Result:
no goals

Proof state:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / τ = -I / (-I * τ) ^ 1

Tactic:
rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)]

Result:
no goals

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

Tactic:
rcases eq_or_ne τ 0 with rfl | hτ

Result:
case inl
z : ℂ
⊢ jacobiTheta₂' z 0 = -2 * ↑π / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)

case inr
z τ : ℂ
hτ : τ ≠ 0
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)