-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
theorem jacobiTheta₂'_functional_equation (z τ : ℂ) :
    jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (cexp (-↑π * I * z ^ 2 * τ⁻¹) * deriv (fun y => -↑π * I * y ^ 2 * τ⁻¹) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [mul_comm, deriv_mul_const_field, deriv_const_mul_field, deriv_pow]

Result:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * (↑2 * z ^ (2 - 1)) * τ⁻¹) * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) * deriv (fun z => cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z => cexp (-↑π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * deriv (fun z => jacobiTheta₂ (z / τ) (-1 / τ)) z)

Tactic:
rw [deriv_mul _ hj.differentiableAt]

Result:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ DifferentiableAt ℂ (fun z => cexp (-↑π * I * z ^ 2 / τ)) z

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

Tactic:
have hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ))
    ((1 / τ) * jacobiTheta₂' (z / τ) (-1 / τ)) z := by
  have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'
  simpa only [mul_comm, one_div] using this.comp z (hasDerivAt_mul_const τ⁻¹)

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ DifferentiableAt ℂ (fun z => cexp (-↑π * I * z ^ 2 / τ)) z

Tactic:
exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * (↑2 * z ^ (2 - 1)) * τ⁻¹) * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
ring_nf

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
⊢ HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z

Tactic:
have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'

Result:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
this : HasDerivAt (fun x => jacobiTheta₂ x (-1 / τ)) (jacobiTheta₂' (z / τ) (-1 / τ)) (z / τ)
⊢ HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z

Proof state:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [jacobiTheta₂'_undef z hτ, jacobiTheta₂'_undef, jacobiTheta₂_undef, mul_zero,
  sub_zero, mul_zero] <;>
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos] <;>
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z => cexp (-↑π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * deriv (fun z => jacobiTheta₂ (z / τ) (-1 / τ)) z) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [hj.deriv]

Result:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z => cexp (-↑π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun z => 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) * deriv (fun z => cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
simp_rw [mul_assoc, deriv_const_mul_field]

Result:
no goals

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

Tactic:
have hτ' : 0 < (-1 / τ).im := by
  rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]
  exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))

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

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z => cexp (-↑π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
erw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _)]

Result:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (cexp (-↑π * I * z ^ 2 * τ⁻¹) * deriv (fun y => -↑π * I * y ^ 2 * τ⁻¹) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))