awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V

Tactic:
continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)

Premises used: Norm.norm, continuousOn_tsum, jacobiTheta₂'_term, Prod.mk, LE.le, _private.0.continuousAt_jacobiTheta₂'.match_1, Prod.fst, jacobiTheta₂', Prod.snd, _private.0.continuousAt_jacobiTheta₂'.match_2
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
refine_1 : ∀ (n : ℤ), ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2) V
refine_2 :
  ∀ (n : ℤ) (x : ℂ × ℂ) (z' τ' : ℂ),
    (z', τ') ∈ V →
      ∀ (hz' : Membership.mem (γ := Set ℂ) {u : ℂ | |u.im| < S} (z', τ').1)
        (hτ' : Membership.mem (γ := Set ℂ) {v : ℂ | T < v.im} (z', τ').2),
        ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V

Tactic:
refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)

Premises used: continuousOn_tsum
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
n : ℤ
refine_1 : Continuous (Y := ℂ) fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2) V

Tactic:
apply Continuous.continuousOn

Premises used: Continuous.continuousOn
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
n : ℤ
⊢ Continuous (Y := ℂ) fun (p : ℂ × ℂ) ↦
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * p.1 + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * p.2)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ'_1 : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
n : ℤ
x : ℂ × ℂ
z' τ' : ℂ
h : (z', τ') ∈ V
hz' : Membership.mem (γ := Set ℂ) {u : ℂ | |u.im| < S} (z', τ').1
hτ' : Membership.mem (γ := Set ℂ) {v : ℂ | T < v.im} (z', τ').2
⊢ ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n

Tactic:
norm_jacobiTheta₂'_term_le hT (le_of_lt hz') (le_of_lt hτ') n

Premises used: le_of_lt, norm_jacobiTheta₂'_term_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ'_1 : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
n : ℤ
x : ℂ × ℂ
z' τ' : ℂ
h : (z', τ') ∈ V
hz' : Membership.mem (γ := Set ℂ) {u : ℂ | |u.im| < S} (z', τ').1
hτ' : Membership.mem (γ := Set ℂ) {v : ℂ | T < v.im} (z', τ').2
⊢ ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n

Tactic:
exact norm_jacobiTheta₂'_term_le hT (le_of_lt hz') (le_of_lt hτ') n

Premises used: le_of_lt, norm_jacobiTheta₂'_term_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr, jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine : ∀ (n : ℤ), jacobiTheta₂_term n z (τ + 2) = jacobiTheta₂_term n z τ
⊢ jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n z (τ + 2) = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, Complex.exp_add]

Premises used: Complex.exp_add, jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      cexp
        ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₃ rw₄ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)

Tactic:
rw [mul_add, Complex.exp_add, this, mul_one]

Premises used: Complex.exp_add, mul_add, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
suffices : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
push_cast :
  (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 =
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (2 * (↑π : ℂ) * I)
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 =
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (2 * (↑π : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
rw₁ : cexp ((↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)) = 1
rw₂ : cexp (2 * (↑π : ℂ) * I) ^ HPow.hPow (β := ℕ) n 2 = 1
rw₃ : HPow.hPow (α := ℂ) 1 (HPow.hPow (β := ℕ) n 2) = 1
rw₄ rw₅ : Eq (α := ℂ) 1 1
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1

Tactic:
rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]

Premises used: one_zpow, Complex.exp_two_pi_mul_I, Complex.exp_int_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr, jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine : ∀ (n : ℤ), jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
⊢ jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * 1) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₃ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₄ :
  cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₅ :
  cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * 1 * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]

Premises used: Int.cast, Complex.exp_add, jacobiTheta₂_term, mul_comm, mul_add, mul_one, Complex.exp_int_mul_two_pi_mul_I
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
rw : ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ
| cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂ z τ

Tactic:
rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]

Premises used: Equiv.addRight, Equiv.tsum_eq, tsum_mul_left, jacobiTheta₂, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
conv_rhs :
  jacobiTheta₂ (z + τ) τ =
    ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ
⊢ jacobiTheta₂ (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂ z τ

Tactic:
conv_rhs => rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]

Premises used: Equiv.addRight, Equiv.tsum_eq, tsum_mul_left, jacobiTheta₂, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ =
    ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr, jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine :
  ∀ (n : ℤ),
    jacobiTheta₂_term n (z + τ) τ =
      cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) n) z τ
⊢ jacobiTheta₂ (z + τ) τ =
    ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp
      (-(↑π : ℂ) * I * (τ + 2 * z) +
        (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ) * z +
          (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ)) 2 * τ))
⊢ jacobiTheta₂_term n (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) n) z τ

Tactic:
simp_rw [jacobiTheta₂_term, ← Complex.exp_add, Equiv.coe_addRight, Int.cast_add]

Premises used: Complex.exp_add, jacobiTheta₂_term, Int.cast_add, Equiv.coe_addRight
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp
      (-(↑π : ℂ) * I * (τ + 2 * z) +
        (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ) * z +
          (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ)) 2 * τ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
rw : ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ
| jacobiTheta₂ (-z) τ

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

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

Tactic:
conv_lhs => rw [jacobiTheta₂, ← Equiv.tsum_eq (Equiv.neg ℤ)]

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

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr, jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine : ∀ (n : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
⊢ ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp
      (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (-(↑n : ℂ)) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₃ :
  cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₄ :
  cexp (2 * ((↑π : ℂ) * (I * (-(↑n : ℂ) * -z))) + (↑π : ℂ) * (I * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))) =
    cexp (2 * ((↑π : ℂ) * (I * ((↑n : ℂ) * z))) + (↑π : ℂ) * (I * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)))
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]

Premises used: Int.cast_neg, jacobiTheta₂_term, mul_assoc, neg_sq, Equiv.neg_apply, neg_mul_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
rw :
  ∑' (a : ℤ), (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term a (-z) τ) =
    jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂ z τ) =
    jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)

Tactic:
rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]

Premises used: jacobiTheta₂_neg_left, 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 : ℂ) → ℂ) τ)
⊢ ∑' (a : ℤ), (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term a (-z) τ) =
    jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)

Tactic:
congr 2 with n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term n (-z) τ) =
    jacobiTheta₂_term n ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)

Tactic:
simp only [jacobiTheta₂_term, mul_neg, ← exp_conj, map_add, map_neg, map_mul, map_ofNat,
    conj_ofReal, conj_I, map_intCast, neg_mul, neg_neg, map_pow]

Premises used: jacobiTheta₂_term, map_ofNat, map_intCast, map_add, neg_neg, map_neg, map_pow, map_mul, Complex.exp_conj, neg_mul, Complex.conj_ofReal, Complex.conj_I, mul_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr, jacobiTheta₂'
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine : ∀ (n : ℤ), jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ

Tactic:
simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]

Premises used: Complex.exp_add, jacobiTheta₂_term, jacobiTheta₂'_term
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp
          ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₁ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₂ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₃ rw₄ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))

Tactic:
rw [mul_add, Complex.exp_add, this, mul_one]

Premises used: Complex.exp_add, mul_add, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
suffices : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))

Tactic:
tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine :
  ∀ (n : ℤ),
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))

Tactic:
refine tsum_congr (fun n ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)

Tactic:
simp only [mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ), exp_int_mul_two_pi_mul_I,
    mul_one]

Premises used: Int.cast, Complex.exp_add, mul_comm, mul_add, mul_one, Complex.exp_int_mul_two_pi_mul_I