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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
refine : ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
⊢ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n p.1 p.2‖ ≤ u n

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (by positivity)

Premises used: mul_le_mul_of_nonneg_left
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))

Tactic:
norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n

Premises used: norm_jacobiTheta₂_term_le, le_of_lt, And.right, And.left
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))

Tactic:
exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n

Premises used: norm_jacobiTheta₂_term_le, le_of_lt, And.right, And.left
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
⊢ ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n

Tactic:
have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n := by
    refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
    refine mul_le_mul_of_nonneg_left ?_ (by positivity)
    exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
simp_rw :
  Summable (α := ℝ) fun (n : ℤ) ↦
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ))))
⊢ Summable u

Tactic:
simp_rw [u, mul_assoc (3 * π)]

Premises used: Real.pi, HMul.hMul, mul_assoc, OfNat.ofNat
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ))))

Tactic:
(summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _

Premises used: Summable.mul_left, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ))))

Tactic:
exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _

Premises used: Summable.mul_left, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable u

Tactic:
have hu_sum : Summable u := by
    simp_rw [u, mul_assoc (3 * π)]
    exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)

Tactic:
(summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_

Premises used: Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
refine :
  ∀ (i : ℤ),
    ‖f i (z, τ)‖ ≤
      HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
        rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * S * (↑|i| : ℝ)))
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)

Tactic:
refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_

Premises used: Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ ∀ (i : ℤ),
    ‖f i (z, τ)‖ ≤
      HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
        rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * S * (↑|i| : ℝ)))

Tactic:
simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hT hz.le hτ'.le

Premises used: norm_jacobiTheta₂_term_le, LT.lt.le, pow_zero, one_mul
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)

Tactic:
have hf_sum : Summable fun n : ℤ ↦ f n (z, τ) := by
    refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_
    simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hT hz.le hτ'.le
-- 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
hf_sum : Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
simpa only [jacobiTheta₂, jacobiTheta₂_fderiv, f, f'] using
    hasFDerivAt_tsum_of_isPreconnected hu_sum hVo hVp hf hu hVmem hf_sum hVmem

Premises used: jacobiTheta₂, jacobiTheta₂_fderiv, hasFDerivAt_tsum_of_isPreconnected
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (z, τ)

Tactic:
(hasFDerivAt_jacobiTheta₂ z hτ).continuousAt

Premises used: hasFDerivAt_jacobiTheta₂, HasFDerivAt.continuousAt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z

Tactic:
((hasFDerivAt_jacobiTheta₂ z hτ).comp (𝕜 := ℂ) z (hasFDerivAt_prodMk_left z τ) :).differentiableAt

Premises used: hasFDerivAt_prodMk_left, jacobiTheta₂, tsum, HasFDerivAt.differentiableAt, HasFDerivAt.comp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ z) τ

Tactic:
((hasFDerivAt_jacobiTheta₂ z hτ).comp τ (hasFDerivAt_prodMk_right z τ)).differentiableAt

Premises used: jacobiTheta₂, hasFDerivAt_jacobiTheta₂, tsum, HasFDerivAt.differentiableAt, HasFDerivAt.comp, hasFDerivAt_prodMk_right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (x y : ℂ × ℂ →L[ℂ] ℂ),
    (x + y : (a : ℂ × ℂ) → ℂ) (1, 0) =
      HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ) ((y : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)

Tactic:
simp only [ContinuousLinearMap.add_apply, forall_const]

Premises used: ContinuousLinearMap.add_apply, forall_const
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (m : ℂ) (x : ℂ × ℂ →L[ℂ] ℂ),
    (m • x : (a : ℂ × ℂ) → ℂ) (1, 0) =
      HSMul.hSMul (α := ℂ) (β := ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) m : ℂ) ((x : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)

Tactic:
apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)

Premises used: ContinuousLinearMap.hasSum, hasSum_jacobiTheta₂_term_fderiv
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)

Tactic:
have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0))
      ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
    apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
n : ℤ
⊢ (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
simp only [jacobiTheta₂_term_fderiv, smul_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul,
      mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term,
      jacobiTheta₂_term, mul_comm _ (cexp _)]

Premises used: ContinuousLinearMap.coe_smul', jacobiTheta₂_term, jacobiTheta₂'_term, jacobiTheta₂_term_fderiv, ContinuousLinearMap.add_apply, MulZeroClass.mul_zero, mul_comm, Complex.exp, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', smul_eq_mul, mul_one, add_zero, smul_add, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
⊢ ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by
    simp only [jacobiTheta₂_term_fderiv, smul_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul,
      mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term,
      jacobiTheta₂_term, mul_comm _ (cexp _)]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)

Tactic:
rw [funext step2] at step1

Premises used: funext
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
step1₁ :
  HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
⊢ ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
rw [funext step2] at step1

Premises used: funext
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ) z

Tactic:
have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z :=
    (((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prodMk_left z τ)).hasDerivAt :)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
step3 : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ) z
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (step3 : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (∑' (b : ℤ), jacobiTheta₂'_term b z τ) z),
    HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
rwa [← step1.tsum_eq] at step3

Premises used: HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
obtain : ∀ (T : ℝ) (hT : 0 < T) (hτ' : T < τ.im), ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨T, hT, hτ'⟩ := exists_between hτ

Premises used: exists_between
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
obtain : ∀ (S : ℝ) (hz : |z.im| < S), ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨S, hz⟩ := exists_gt |im z|

Premises used: abs, Complex.im, NoMaxOrder.exists_gt
-- 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}
⊢ IsOpen V

Tactic:
have hVo : IsOpen V := ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _
    isOpen_Iio).prod (continuous_im.isOpen_preimage _ isOpen_Ioi)
-- 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
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)

Premises used: And.intro, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- 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
refine : ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
refine ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)
-- 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| : ℝ)))
⊢ Summable u

Tactic:
simpa only [u, mul_assoc, pow_one]
      using (summable_pow_mul_jacobiTheta₂_term_bound S hT 1).mul_left (2 * π)

Premises used: Real.pi, HMul.hMul, mul_assoc, Summable.mul_left, pow_one, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat