awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂' (z + τ) τ =
      cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
inr :
  ∀ (hτ : 0 < τ.im),
    jacobiTheta₂' (z + τ) τ =
      cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)

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

Premises used: Complex.im, le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl : jacobiTheta₂' (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * 0)
inl₁ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (0 - 2 * (↑π : ℂ) * I * 0)
inl₂ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * HSub.hSub (α := ℂ) 0 0
inl₃ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * 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]

Premises used: sub_zero, MulZeroClass.mul_zero, jacobiTheta₂_undef, jacobiTheta₂'_undef
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    cexp
      ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
          (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
        -(↑π : ℂ) * I * (τ + 2 * z))
| cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
    (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ) -
      2 * (↑π : ℂ) * I *
        cexp (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ))

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

Premises used: Complex.exp_add, mul_assoc, Int.cast_add, sub_mul, mul_comm, mul_add, add_sub_cancel_right, mul_one, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
conv_rhs :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
            (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
          -(↑π : ℂ) * I * (τ + 2 * z))
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
      (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) *
          cexp
            (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ) -
        2 * (↑π : ℂ) * I *
          cexp
            (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(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]

Premises used: Complex.exp_add, mul_assoc, Int.cast_add, sub_mul, mul_comm, mul_add, add_sub_cancel_right, mul_one, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
e_a :
  2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
        (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
      -(↑π : ℂ) * I * (τ + 2 * z)
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
            (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
          -(↑π : ℂ) * I * (τ + 2 * z))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
        (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
      -(↑π : ℂ) * I * (τ + 2 * z)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
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:
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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 τ)
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 τ)
⊢ 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]

Premises used: Equiv.subRight, Equiv.tsum_eq, tsum_mul_left, funext, jacobiTheta₂', OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 τ)
⊢ 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:
simp only [jacobiTheta₂, jacobiTheta₂', Equiv.subRight_apply, sub_add_cancel,
    (hasSum_jacobiTheta₂'_term z hτ).summable.tsum_sub
    ((hasSum_jacobiTheta₂_term z hτ).summable.mul_left _), tsum_mul_left]

Premises used: hasSum_jacobiTheta₂_term, tsum_mul_left, jacobiTheta₂, hasSum_jacobiTheta₂'_term, HasSum.summable, Summable.mul_left, Equiv.subRight_apply, jacobiTheta₂', Summable.tsum_sub, sub_add_cancel
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
rw :
  Eq (α := ℂ) (∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ)
    (∑' (b : ℤ), -jacobiTheta₂'_term b z τ)
⊢ jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ

Tactic:
rw [jacobiTheta₂', jacobiTheta₂', ← tsum_neg, ← (Equiv.neg ℤ).tsum_eq]

Premises used: Equiv.neg, Equiv.tsum_eq, Int, tsum_neg, jacobiTheta₂'
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
e_f : ∀ (n : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = -jacobiTheta₂'_term n z τ
⊢ Eq (α := ℂ) (∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ)
    (∑' (b : ℤ), -jacobiTheta₂'_term b z τ)

Tactic:
congr 1 with n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
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 * τ)
⊢ 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 * τ))

Tactic:
rw [Equiv.neg_apply, ← neg_mul]

Premises used: Equiv.neg_apply, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
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 * τ)
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 * τ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
rw :
  Eq (α := ℂ) (∑' (b : ℤ), -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term b z τ))
    (∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ))
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂' z τ) =
    jacobiTheta₂' ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)

Tactic:
rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]

Premises used: jacobiTheta₂'_neg_left, tsum_neg, neg_inj, jacobiTheta₂', Complex.conj_tsum
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
e_f :
  ∀ (n : ℤ),
    -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term n z τ) =
      jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
⊢ Eq (α := ℂ) (∑' (b : ℤ), -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term b z τ))
    (∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ))

Tactic:
congr 1 with n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
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 : ℂ) → ℂ) τ : ℂ))
⊢ -(starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'_term n z τ) =
    jacobiTheta₂'_term n (-(starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(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]

Premises used: jacobiTheta₂_term, jacobiTheta₂'_term, Complex.ofReal_intCast, map_add, map_pow, map_mul, Complex.exp_conj, Complex.conj_ofReal, Complex.ofReal_ofNat, Complex.conj_I
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
⊢ -((↑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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂ z τ =
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
inr :
  ∀ (hτ : 0 < τ.im),
    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 / τ)

Tactic:
rcases le_or_gt (im τ) 0 with hτ | hτ

Premises used: Complex.im, le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
rw : 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)
⊢ (-1 / τ).im ≤ 0

Tactic:
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Premises used: neg_div, neg_nonpos, one_div, Complex.inv_im, Complex.neg_im
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)

Tactic:
div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Premises used: Iff.mpr, neg_nonneg, Complex.normSq_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)

Tactic:
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Premises used: Iff.mpr, neg_nonneg, Complex.normSq_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-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 τ)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
inl₂ inl₃ : Eq (α := ℂ) 0 0
⊢ jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]

Premises used: MulZeroClass.mul_zero, jacobiTheta₂_undef
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-I * τ).re

Tactic:
simpa only [neg_mul, neg_re, mul_re, I_re, zero_mul, I_im, one_mul, zero_sub, neg_neg] using hτ

Premises used: Complex.mul_re, MulZeroClass.zero_mul, neg_neg, Complex.I_re, Complex.I_im, Complex.neg_re, neg_mul, one_mul, zero_sub
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 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τ
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
rw 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)
⊢ ∑' (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:
rw [tsum_exp_neg_quadratic h2]

Premises used: Complex.tsum_exp_neg_quadratic
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
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 / τ)))
⊢ 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:
simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]

Premises used: Complex.exp_add, mul_assoc, tsum_mul_left, Complex.exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
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 / τ)))
⊢ 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:
congr 2 with n : 1
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
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 / τ))
⊢ 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 1
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
e_a :
  HPow.hPow (β := ℕ) ((↑n : ℂ) + HPow.hPow (β := ℕ) I 2 * z) 2 / τ =
    HPow.hPow (β := ℕ) I 2 * (-HPow.hPow (β := ℕ) z 2 + (↑n : ℂ) * (z * 2 + -(↑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 / τ))

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
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 * τ⁻¹
⊢ HPow.hPow (β := ℕ) ((↑n : ℂ) + HPow.hPow (β := ℕ) I 2 * z) 2 / τ =
    HPow.hPow (β := ℕ) I 2 * (-HPow.hPow (β := ℕ) z 2 + (↑n : ℂ) * (z * 2 + -(↑n : ℂ))) / τ

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
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 * τ⁻¹
⊢ (↑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:
simp_rw [I_sq, I_pow_four]

Premises used: Complex.I_pow_four, Complex.I_sq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
e_a : (↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 = -(↑π : ℂ) * I * HPow.hPow (β := ℕ) 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 / τ)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))

Tactic:
congr 3
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ (↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2 = -(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ

Tactic:
ring