awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
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 τ)
have inr : cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
    ∑' (c : ℤ),
      (jacobiTheta₂'_term (HAdd.hAdd (α := ℤ) (β := ℤ) ((Equiv.subRight 1 : (a : ℤ) → ℤ) c : ℤ) (1 : ℤ)) z τ -
        2 * (↑π : ℂ) * I *
          jacobiTheta₂_term (HAdd.hAdd (α := ℤ) (β := ℤ) ((Equiv.subRight 1 : (a : ℤ) → ℤ) c : ℤ) (1 : ℤ)) z τ) =
  cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
Tactic: rw [jacobiTheta₂', funext this, tsum_mul_left, ← (Equiv.subRight (1 : ℤ)).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ
have rw : Eq (α := ℂ) (∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ)
  (∑' (b : ℤ), -jacobiTheta₂'_term b z τ)
Tactic: rw [jacobiTheta₂', jacobiTheta₂', ← tsum_neg, ← (Equiv.neg ℤ).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ Eq (α := ℂ) (∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ)
    (∑' (b : ℤ), -jacobiTheta₂'_term b z τ)
have e_f : ∀ (n : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = -jacobiTheta₂'_term n z τ
Tactic: congr 1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    -(2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have e_f : 2 * (↑π : ℂ) * I * (↑(-n) : ℂ) *
    cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
  -(2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: rw [Equiv.neg_apply, ← neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑(-n) : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
    -(2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
have e_f : 2 * (↑π : ℂ) * I * -(↑n : ℂ) *
    cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (-(↑n : ℂ)) 2 * τ) =
  -(2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂' z τ) =
    jacobiTheta₂' ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
have rw : Eq (α := ℂ) (∑' (b : ℤ), -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term b z τ))
  (∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ))
Tactic: rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ Eq (α := ℂ) (∑' (b : ℤ), -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term b z τ))
    (∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ))
have e_f : ∀ (n : ℤ),
  -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term n z τ) =
    jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
Tactic: congr 1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term n z τ) =
    jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
have e_f : -((↑2 : ℂ) * (↑π : ℂ) * -I * (↑(↑n : ℝ) : ℂ) *
      cexp
        (HMul.hMul (β := ℂ) ((↑2 : ℂ) * (↑π : ℂ) * -I * (↑(↑n : ℝ) : ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) +
          HMul.hMul (β := ℂ) ((↑π : ℂ) * -I * HPow.hPow (β := ℕ) (↑(↑n : ℝ) : ℂ) 2)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) τ : ℂ))) =
  (↑2 : ℂ) * (↑π : ℂ) * I * (↑(↑n : ℝ) : ℂ) *
    cexp
      (HMul.hMul (β := ℂ) ((↑2 : ℂ) * (↑π : ℂ) * I * (↑(↑n : ℝ) : ℂ)) (-(starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) +
        HMul.hMul (β := ℂ) ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑(↑n : ℝ) : ℂ) 2) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ : ℂ))
Tactic: simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, map_mul, ← Complex.exp_conj, map_add, map_mul,
    ← ofReal_intCast, ← ofReal_ofNat, map_pow, conj_ofReal, conj_I]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have inl : ∀ (hτ : τ.im ≤ 0),
  jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
Tactic: rcases le_or_gt (im τ) 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂ z τ =
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have inr : ∀ (hτ : 0 < τ.im),
  jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
Tactic: rcases le_or_gt (im τ) 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0
have rw : 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)
Tactic: rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have this : (-1 / τ).im ≤ 0
Tactic: have : (-1 / τ).im ≤ 0 := by
      rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]
      exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have inl : 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
Tactic: rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
inl : 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have inl₁ : 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * 0
Tactic: rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
inl : 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
inl₁ : 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * 0
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
have inl₂ : Eq (α := ℂ) 0 0
Tactic: rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∑' (n : ℤ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have h2 : 0 < (-I * τ).re
Tactic: have h2 : 0 < (-I * τ).re := by
    simpa only [neg_mul, neg_re, mul_re, I_re, zero_mul, I_im, one_mul, zero_sub, neg_neg] using hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ)) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
have rw : 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
  1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
Tactic: rw [tsum_exp_neg_quadratic h2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have simp_rw : 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
  1 / (-I * τ) ^ (1 / 2) *
    ∑' (x : ℤ),
      cexp
        ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
          (2 * (↑π : ℂ) * I * (↑x : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑x : ℂ) 2 * (-1 / τ)))
Tactic: simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    1 / (-I * τ) ^ (1 / 2) *
      ∑' (x : ℤ),
        cexp
          ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
            (2 * (↑π : ℂ) * I * (↑x : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑x : ℂ) 2 * (-1 / τ)))
have e_a : ∀ (n : ℤ),
  cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    cexp
      ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ)))
Tactic: congr 2 with n : 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    cexp
      ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ)))
have e_a : -(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2 =
  (↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
    (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ -(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2 =
    (↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 +
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have e_a : HPow.hPow (β := ℕ) ((↑n : ℂ) + HPow.hPow (β := ℕ) I 2 * z) 2 / τ =
  HPow.hPow (β := ℕ) I 2 * (-HPow.hPow (β := ℕ) z 2 + (↑n : ℂ) * (z * 2 + -(↑n : ℂ))) / τ
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ HPow.hPow (β := ℕ) ((↑n : ℂ) + HPow.hPow (β := ℕ) I 2 * z) 2 / τ =
    HPow.hPow (β := ℕ) I 2 * (-HPow.hPow (β := ℕ) z 2 + (↑n : ℂ) * (z * 2 + -(↑n : ℂ))) / τ
have e_a : (↑n : ℂ) * HPow.hPow (β := ℕ) I 2 * z * τ⁻¹ * 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ⁻¹ +
    HPow.hPow (β := ℕ) I 4 * HPow.hPow (β := ℕ) z 2 * τ⁻¹ =
  (↑n : ℂ) * HPow.hPow (β := ℕ) I 2 * z * τ⁻¹ * 2 -
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * HPow.hPow (β := ℕ) I 2 * τ⁻¹ -
    HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) z 2 * τ⁻¹
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ (↑n : ℂ) * HPow.hPow (β := ℕ) I 2 * z * τ⁻¹ * 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ⁻¹ +
      HPow.hPow (β := ℕ) I 4 * HPow.hPow (β := ℕ) z 2 * τ⁻¹ =
    (↑n : ℂ) * HPow.hPow (β := ℕ) I 2 * z * τ⁻¹ * 2 -
        HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * HPow.hPow (β := ℕ) I 2 * τ⁻¹ -
      HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) z 2 * τ⁻¹
have e_a : HMul.hMul (α := ℂ) (↑n : ℂ) (-1) * z * τ⁻¹ * 2 + HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ⁻¹ +
    1 * HPow.hPow (β := ℕ) z 2 * τ⁻¹ =
  HMul.hMul (α := ℂ) (↑n : ℂ) (-1) * z * τ⁻¹ * 2 - HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * -1 * τ⁻¹ -
    -1 * HPow.hPow (β := ℕ) z 2 * τ⁻¹
Tactic: simp_rw [I_sq, I_pow_four]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
      ∑' (n : ℤ),
        cexp
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have e_a : (↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 = -(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have _ : ∑' (n : ℤ), cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ)) =
  1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
Tactic: calc
  _ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) :=
    tsum_congr (fun n ↦ by ring_nf)
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
    rw [tsum_exp_neg_quadratic h2]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) := by
    simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
    congr 2 with n : 1; congr 1
    field_simp
    ring_nf
    simp_rw [I_sq, I_pow_four]
    ring_nf
  _ = _ := by
    congr 3
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
_ :
  ∑' (n : ℤ), cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ)) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
⊢ ∑' (n : ℤ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have _₁ : 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
  1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
    ∑' (n : ℤ),
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
Tactic: calc
  _ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) :=
    tsum_congr (fun n ↦ by ring_nf)
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
    rw [tsum_exp_neg_quadratic h2]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) := by
    simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
    congr 2 with n : 1; congr 1
    field_simp
    ring_nf
    simp_rw [I_sq, I_pow_four]
    ring_nf
  _ = _ := by
    congr 3
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
_ :
  ∑' (n : ℤ), cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ)) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
_₁ :
  1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
⊢ ∑' (n : ℤ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
have _₂ : 1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
    ∑' (n : ℤ),
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ)) =
  1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
    ∑' (n : ℤ),
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
Tactic: calc
  _ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) :=
    tsum_congr (fun n ↦ by ring_nf)
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
    rw [tsum_exp_neg_quadratic h2]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) := by
    simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
    congr 2 with n : 1; congr 1
    field_simp
    ring_nf
    simp_rw [I_sq, I_pow_four]
    ring_nf
  _ = _ := by
    congr 3
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have inl : ∀ (hτ : τ.im ≤ 0),
  jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
Tactic: rcases le_or_gt (im τ) 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂' z τ =
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have inr : ∀ (hτ : 0 < τ.im),
  jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
Tactic: rcases le_or_gt (im τ) 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have inl : (-1 / τ).im ≤ 0
Tactic: rw [jacobiTheta₂'_undef z hτ, jacobiTheta₂'_undef, jacobiTheta₂_undef, mul_zero,
      sub_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0
have inl : 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)
Tactic: rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 / τ).im
have rw : 0 < HDiv.hDiv (β := ℝ) τ.im ((normSq : (a : ℂ) → ℝ) τ : ℝ)
Tactic: rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have hτ' : 0 < (-1 / τ).im
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τ)))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
⊢ HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
have this : HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x (-1 / τ)) (jacobiTheta₂' (z / τ) (-1 / τ)) (z / τ)
Tactic: have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
have hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
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 τ⁻¹)