awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
simp_rw :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop
⊢ Tendsto
    (HSub.hSub (α := ℕ → ℝ) (fun (x : ℕ) ↦ -π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))
      fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
    atTop atBot

Tactic:
simp_rw [← tendsto_neg_atTop_iff, Pi.sub_apply]

Premises used: Filter.tendsto_neg_atTop_iff, Pi.sub_apply
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
h :
  ∀ (n : ℕ), -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑n : ℝ))
| Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop

Tactic:
enter [1, n]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k n : ℕ
⊢ -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑n : ℝ)) =
    (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k n : ℕ
h : (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))
| -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑n : ℝ))

Tactic:
rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
h : ∀ (n : ℕ), (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))
| Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop

Tactic:
enter [1, n]
    rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
conv : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))) atTop atTop
⊢ Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop

Tactic:
conv =>
    enter [1, n]
    rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))) atTop atTop

Tactic:
tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_natCast_atTop_atTop, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
refine : Tendsto (β := ℝ) (fun (n : ℕ) ↦ π * T * (↑n : ℝ)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))) atTop atTop

Tactic:
refine tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_natCast_atTop_atTop, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ π * T * (↑n : ℝ)) atTop atTop

Tactic:
tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)

Premises used: Filter.Tendsto.const_mul_atTop, Real.pi_pos, mul_pos, tendsto_natCast_atTop_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ π * T * (↑n : ℝ)) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)

Premises used: Filter.Tendsto.const_mul_atTop, Real.pi_pos, mul_pos, tendsto_natCast_atTop_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ↔ 0 < τ.im

Tactic:
Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, Iff.symm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
refine_1 : ∀ (hτ : 0 < τ.im), Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
refine_2 : ∀ (h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ), 0 < τ.im
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ↔ 0 < τ.im

Tactic:
refine Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, Iff.symm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
(summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_

Premises used: abs, Complex.im, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
refine_1 :
  ∀ (i : ℤ),
    ‖jacobiTheta₂_term i z τ‖ ≤
      HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * |z.im| * (↑|i| : ℝ)))
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_

Premises used: abs, Complex.im, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (i : ℤ),
    ‖jacobiTheta₂_term i z τ‖ ≤
      HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * |z.im| * (↑|i| : ℝ)))

Tactic:
simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl

Premises used: norm_jacobiTheta₂_term_le, le_rfl, pow_zero, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
refine_2 : ∀ (hτ : τ.im ≤ 0), False
⊢ 0 < τ.im

Tactic:
by_contra! hτ
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ : τ.im ≤ 0
refine_2 : ∀ (hτ : τ.im < 0), False
refine_2₁ : ∀ (hτ : τ.im = 0), False
⊢ False

Tactic:
rcases lt_or_eq_of_le hτ with hτ | hτ

Premises used: lt_or_eq_of_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
⊢ Tendsto (fun (x : ℕ) ↦ Norm.norm (E := ℂ) (((fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) x))
    atTop (𝓝 (Norm.norm (E := ℂ) 0))

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
h :
  Tendsto (fun (x : ℕ) ↦ Norm.norm (E := ℂ) (((fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) x))
    atTop (𝓝 (Norm.norm (E := ℂ) 0))
⊢ False

Tactic:
atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
h :
  Tendsto (fun (x : ℕ) ↦ Norm.norm (E := ℂ) (((fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) x))
    atTop (𝓝 (Norm.norm (E := ℂ) 0))
⊢ False

Tactic:
exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
⊢ False

Tactic:
suffices Tendsto (fun n : ℕ ↦ ‖jacobiTheta₂_term ↑n z τ‖) atTop atTop by
        replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
        exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
refine_2 :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop

Tactic:
simp only [norm_jacobiTheta₂_term, Int.cast_natCast]

Premises used: Int.cast_natCast, norm_jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
h₁ : ∀ (n : ℕ), rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
| Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop

Tactic:
enter [1, n]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
n : ℕ
⊢ -π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im =
    (↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
n : ℕ
h₁ : rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))
| rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)

Tactic:
rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
h₁ : ∀ (n : ℕ), rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))
| Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop

Tactic:
enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop

Tactic:
conv =>
        enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))) atTop atTop

Tactic:
tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)

Premises used: Real.tendsto_exp_atTop, Real.exp, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (-π * τ.im) - 2 * π * z.im) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))) atTop atTop

Tactic:
refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)

Premises used: Real.tendsto_exp_atTop, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (-π * τ.im) - 2 * π * z.im) atTop atTop

Tactic:
tendsto_atTop_add_const_right _ _ (tendsto_natCast_atTop_atTop.atTop_mul_const
        (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, Filter.Tendsto.atTop_mul_const, Real.pi_pos, neg_lt_zero, tendsto_natCast_atTop_atTop, mul_pos_of_neg_of_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (-π * τ.im) - 2 * π * z.im) atTop atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ (tendsto_natCast_atTop_atTop.atTop_mul_const
        (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, Filter.Tendsto.atTop_mul_const, Real.pi_pos, neg_lt_zero, tendsto_natCast_atTop_atTop, mul_pos_of_neg_of_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
⊢ Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))

Tactic:
simp_rw [← summable_norm_iff (E := ℂ), norm_jacobiTheta₂_term, hτ, mul_zero, zero_sub] at h

Premises used: norm_jacobiTheta₂_term, MulZeroClass.mul_zero, summable_norm_iff, zero_sub
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
refine_2 : ∀ (hz : z.im < 0), False
refine_2₁ : ∀ (hz : z.im = 0), False
refine_2₂ : ∀ (hz : 0 < z.im), False
⊢ False

Tactic:
rcases lt_trichotomy (im z) 0 with hz | hz | hz

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : z.im < 0
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) atTop (𝓝 0)

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)

Tactic:
simp_rw [Function.comp_def, Int.cast_natCast] at h

Premises used: Int.cast_natCast, Function.comp_def
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ False

Tactic:
atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, OfNat.ofNat, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop atTop
⊢ False

Tactic:
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, OfNat.ofNat, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop atTop

Tactic:
tendsto_exp_atTop.comp ?_

Premises used: Real.tendsto_exp_atTop, Real.exp, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -(2 * π * (↑x : ℝ) * z.im)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop atTop

Tactic:
refine tendsto_exp_atTop.comp ?_

Premises used: Real.tendsto_exp_atTop, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ 2 * (π * ((↑x : ℝ) * z.im))) atTop atBot
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -(2 * π * (↑x : ℝ) * z.im)) atTop atTop

Tactic:
simp only [tendsto_neg_atTop_iff, mul_assoc]

Premises used: mul_assoc, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ π * ((↑x : ℝ) * z.im)) atTop atBot
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ 2 * (π * ((↑x : ℝ) * z.im))) atTop atBot

Tactic:
apply Filter.Tendsto.const_mul_atBot two_pos

Premises used: Filter.Tendsto.const_mul_atBot
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ π * ((↑x : ℝ) * z.im)) atTop atBot

Tactic:
(tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos

Premises used: Filter.Tendsto.atTop_mul_const_of_neg, Real.pi_pos, tendsto_natCast_atTop_atTop, Filter.Tendsto.const_mul_atBot
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ π * ((↑x : ℝ) * z.im)) atTop atBot

Tactic:
exact (tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos

Premises used: Filter.Tendsto.atTop_mul_const_of_neg, Real.pi_pos, tendsto_natCast_atTop_atTop, Filter.Tendsto.const_mul_atBot
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : z.im = 0
refine_2 : ∀ (h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))), False
⊢ False

Tactic:
revert h
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ ∀ (h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))), False

Tactic:
simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero

Premises used: MulZeroClass.mul_zero, summable_const_iff, Real.exp_zero, one_ne_zero, neg_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : 0 < z.im
x x_1 : ℕ
⊢ Eq (α := ℤ) ((fun (x : ℕ) ↦ (-(↑x : ℤ) : ℤ)) x) ((fun (x : ℕ) ↦ (-(↑x : ℤ) : ℤ)) x_1) → x = x_1

Tactic:
simp only [neg_inj, Nat.cast_inj, imp_self]

Premises used: Nat.cast_inj, imp_self, neg_inj
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : 0 < z.im
⊢ Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)

Tactic:
have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (x : ℕ) ↦ -(↑x : ℤ)) atTop (𝓝 0)

Tactic:
replace h := (h.comp_injective this).tendsto_atTop_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (x : ℕ) ↦ -(↑x : ℤ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)

Tactic:
simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h

Premises used: Int.cast_neg, Int.cast_natCast, neg_neg, Function.comp_def, neg_mul, mul_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
⊢ False

Tactic:
atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, OfNat.ofNat, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop atTop
⊢ False

Tactic:
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

Premises used: Filter.NeBot.ne, Filter.Tendsto.disjoint, Filter.atTop_neBot, disjoint_nhds_atTop, Iff.mp, OfNat.ofNat, disjoint_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop atTop

Tactic:
tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
          (mul_pos two_pos pi_pos)).atTop_mul_const hz)

Premises used: Filter.Tendsto.const_mul_atTop, Filter.Tendsto.atTop_mul_const, Real.tendsto_exp_atTop, Real.pi_pos, Real.exp, mul_pos, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop atTop

Tactic:
exact tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
          (mul_pos two_pos pi_pos)).atTop_mul_const hz)

Premises used: Filter.Tendsto.const_mul_atTop, Filter.Tendsto.atTop_mul_const, Real.tendsto_exp_atTop, Real.pi_pos, mul_pos, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp