-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂'_add_left' (z τ : ℂ) :
    jacobiTheta₂' (z + τ) τ =
      cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * π * I * jacobiTheta₂ z τ)

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ cexp (-↑π * I * (τ + 2 * z)) *
      ∑' (c : ℤ),
        (jacobiTheta₂'_term ((Equiv.subRight 1) c + 1) z τ -
          2 * ↑π * I * jacobiTheta₂_term ((Equiv.subRight 1) c + 1) z τ) =
    cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
simp only [jacobiTheta₂, jacobiTheta₂', Equiv.subRight_apply, sub_add_cancel,
  tsum_sub (hasSum_jacobiTheta₂'_term z hτ).summable
  ((hasSum_jacobiTheta₂_term z hτ).summable.mul_left _), tsum_mul_left]

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ jacobiTheta₂'_term n (z + τ) τ =
    cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)

Tactic:
simp only [jacobiTheta₂'_term, jacobiTheta₂_term]

Result:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z)) *
      (2 * ↑π * I * ↑(n + 1) * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ) -
        2 * ↑π * I * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ))

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

Tactic:
simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]

Result:
no goals

Proof state:
case e_a.e_z
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ =
    (2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z)

Tactic:
ring

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    2 * ↑π * I * ↑n * cexp ((2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z))

Tactic:
congr 2

Result:
case e_a.e_z
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ =
    (2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z)

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

Tactic:
rcases le_or_lt τ.im 0 with hτ | hτ

Result:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

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

Proof state:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z)) *
      (2 * ↑π * I * ↑(n + 1) * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ) -
        2 * ↑π * I * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ))

Tactic:
conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
  mul_add, mul_one, add_sub_cancel_right]

Result:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    2 * ↑π * I * ↑n * cexp ((2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z))

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

Tactic:
have (n : ℤ) : jacobiTheta₂'_term n (z + τ) τ =
    cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ -
    2 * π * I * jacobiTheta₂_term (n + 1) z τ) := by
  simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
  conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
    mul_add, mul_one, add_sub_cancel_right]
  congr 2
  ring

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
rw [jacobiTheta₂', funext this, tsum_mul_left, ← (Equiv.subRight (1 : ℤ)).tsum_eq]

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ cexp (-↑π * I * (τ + 2 * z)) *
      ∑' (c : ℤ),
        (jacobiTheta₂'_term ((Equiv.subRight 1) c + 1) z τ -
          2 * ↑π * I * jacobiTheta₂_term ((Equiv.subRight 1) c + 1) z τ) =
    cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)