awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
this : (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
simp_rw : jacobiTheta (2 + (↑τ : ℂ)) = jacobiTheta (↑τ : ℂ)
⊢ jacobiTheta (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = jacobiTheta (↑τ : ℂ)

Tactic:
simp_rw [this, jacobiTheta_two_add]

Premises used: jacobiTheta_two_add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
suffices : (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
⊢ jacobiTheta (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = jacobiTheta (↑τ : ℂ)

Tactic:
suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
⊢ HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2

Tactic:
have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
this : HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2
simp_rw : (↑(↑2 : ℝ) : ℂ) + (↑τ : ℂ) = 2 + (↑τ : ℂ)
⊢ (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)

Tactic:
simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]

Premises used: UpperHalfPlane.coe_vadd, UpperHalfPlane.modular_T_zpow_smul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
this : HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 2 + (↑τ : ℂ) = 2 + (↑τ : ℂ)
⊢ (↑(↑2 : ℝ) : ℂ) + (↑τ : ℂ) = 2 + (↑τ : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
⊢ (↑τ : ℂ) ≠ 0

Tactic:
have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
rw : ¬-I * (↑τ : ℂ) = 0 ∨ ¬1 / 2 ≠ 0
⊢ (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]

Premises used: Complex.cpow_eq_zero_iff, Ne, not_and_or
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
⊢ ¬-I * (↑τ : ℂ) = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0

Premises used: Iff.mpr, Complex.I_ne_zero, neg_ne_zero, Or.inl, mul_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
⊢ ¬-I * (↑τ : ℂ) = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0

Premises used: Iff.mpr, Complex.I_ne_zero, neg_ne_zero, Or.inl, mul_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
⊢ (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0

Tactic:
have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
    rw [Ne, cpow_eq_zero_iff, not_and_or]
    exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
simp_rw : jacobiTheta₂ (↑0 : ℂ) (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ (↑0 : ℂ) (↑τ : ℂ)
⊢ jacobiTheta (↑(ModularGroup.S • τ) : ℂ) = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta (↑τ : ℂ)

Tactic:
simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂, ← ofReal_zero]

Premises used: UpperHalfPlane.modular_S_smul, Complex.ofReal_zero, jacobiTheta_eq_jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
simp_rw :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 0 2 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₁ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * 0 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₂ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (0 / (↑τ : ℂ)) * jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₃ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp 0 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
simp_rw₄ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * 1 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
simp_rw₅ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
simp_rw₆ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2)) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
simp_rw₇ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 / (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
simp_rw₈ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = 1 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
simp_rw₉ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
simp_rw₁₀ : jacobiTheta₂ 0 (-(↑τ : ℂ)⁻¹) = jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
simp_rw₁₁ : jacobiTheta₂ 0 (-(↑τ : ℂ)⁻¹) = jacobiTheta₂ 0 (-(1 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)

Tactic:
simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div,
    Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div, div_self h1, one_mul,
    inv_neg, neg_div, one_div]

Premises used: neg_div, jacobiTheta₂_functional_equation, UpperHalfPlane.coe, Complex.exp_zero, mul_assoc, zero_div, inv_neg, MulZeroClass.mul_zero, two_ne_zero, mul_one_div, one_div, mul_one, OfNat.ofNat, zero_pow, one_mul, div_self
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
⊢ y < 1

Tactic:
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
(le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)

Premises used: LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
refine_1 : ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ = y ^ HPow.hPow (β := ℕ) n 2
refine_2 : y ^ HPow.hPow (β := ℕ) n 2 ≤ rexp (-π * τ.im) ^ n.natAbs
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
refine (le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)

Premises used: LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
refine_1 : rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ = y ^ HPow.hPow (β := ℕ) n 2

Tactic:
rw [norm_exp]

Premises used: Complex.norm_exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
push_cast :
  (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ * I)
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) : ℂ) * (τ * I)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ * I)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * -τ.im = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
rw [(by push_cast; ring : (π * I * n ^ 2 * τ : ℂ) = (π * n ^ 2 : ℝ) * (τ * I)),
        re_ofReal_mul, mul_I_re]

Premises used: Complex.mul_I_re, Complex.re_ofReal_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * -τ.im = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
have : (π * I * n ^ 2 * τ : ℂ).re = -π * τ.im * (n : ℝ) ^ 2 := by
      rw [(by push_cast; ring : (π * I * n ^ 2 * τ : ℂ) = (π * n ^ 2 : ℝ) * (τ * I)),
        re_ofReal_mul, mul_I_re]
      ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this :
  ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
refine_1 :
  ∀ (m : ℕ) (hm : HPow.hPow (β := ℕ) n 2 = (↑m : ℤ)),
    rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n)

Premises used: Int.eq_ofNat_of_zero_le, sq_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this :
  ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
m : ℕ
hm : HPow.hPow (β := ℕ) n 2 = (↑m : ℤ)
refine_1 : rexp (-π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) = y ^ HPow.hPow (β := ℕ) n 2
refine_1₁ : rexp (-π * τ.im) ^ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 = y ^ HPow.hPow (β := ℕ) n 2
refine_1₂ : HPow.hPow (β := ℝ) (rexp (-π * τ.im)) (↑(HPow.hPow (β := ℕ) n 2) : ℝ) = y ^ HPow.hPow (β := ℕ) n 2
refine_1₃ : rexp (-π * τ.im) ^ HPow.hPow (β := ℕ) n 2 = y ^ HPow.hPow (β := ℕ) n 2
refine_1₄ : HPow.hPow (β := ℤ) (rexp (-π * τ.im)) (↑m : ℤ) = HPow.hPow (β := ℤ) y (↑m : ℤ)
refine_1₅ refine_1₆ : rexp (-π * τ.im) ^ m = rexp (-π * τ.im) ^ m
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2

Tactic:
rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]

Premises used: zpow_natCast, Real.exp_mul, Int.cast_pow, Real.rpow_intCast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
rw : HPow.hPow (β := ℕ) n 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑n.natAbs : ℤ) 2
rw₁ rw₂ : HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) n 2
⊢ HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)

Tactic:
rw [Nat.cast_pow, Int.natAbs_sq]

Premises used: Int.natAbs_sq, Nat.cast_pow
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)

Tactic:
have : n ^ 2 = (n.natAbs ^ 2 :) := by rw [Nat.cast_pow, Int.natAbs_sq]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
refine_2 : y ^ HPow.hPow (β := ℕ) n.natAbs 2 ≤ rexp (-π * τ.im) ^ n.natAbs
⊢ y ^ HPow.hPow (β := ℕ) n 2 ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
rw [this, zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
⊢ y ^ HPow.hPow (β := ℕ) n.natAbs 2 ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)

Premises used: Eq.rec, LT.lt.le, pow_le_pow_of_le_one, sq, Int.natAbs, Nat.le_mul_self, Eq.symm, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
⊢ y ^ HPow.hPow (β := ℕ) n.natAbs 2 ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)

Premises used: LT.lt.le, pow_le_pow_of_le_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)

Tactic:
have := hasSum_jacobiTheta₂_term 0 hτ
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)
⊢ HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)

Tactic:
simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this

Premises used: jacobiTheta₂_term, zero_add, MulZeroClass.mul_zero, jacobiTheta_eq_jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
⊢ HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑n : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ))

Tactic:
have := this.nat_add_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑n : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ))
⊢ HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ) -
      ∑ i ∈ Finset.range 1,
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑i : ℤ) : ℂ) 2 * τ) +
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑i : ℤ)) : ℂ) 2 * τ)))

Tactic:
rw [← hasSum_nat_add_iff' 1] at this

Premises used: hasSum_nat_add_iff', OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ) * 2)
    (jacobiTheta τ + (1 - HMul.hMul (α := ℂ) 1 2))
⊢ 1 - HMul.hMul (α := ℂ) 1 2 = -1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ) -
      ∑ i ∈ Finset.range 1,
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑i : ℤ) : ℂ) 2 * τ) +
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑i : ℤ)) : ℂ) 2 * τ)))
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
    (jacobiTheta τ - 1)

Tactic:
simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
    Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
    Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ← sub_eq_add_neg,
    Nat.cast_add, Nat.cast_one] at this

Premises used: add_sub_assoc, Int.cast_neg, Int.cast_natCast, Complex.exp_zero, Int.cast_zero, MulZeroClass.zero_mul, sub_eq_add_neg, neg_sq, Finset.sum_range_one, sq, MulZeroClass.mul_zero, Nat.cast_add, Nat.cast_zero, OfNat.ofNat, neg_zero, Nat.cast_one, mul_two
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
    (jacobiTheta τ - 1)
⊢ HasSum (fun (i : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 * τ) * 2 / 2)
    ((jacobiTheta τ - 1) / 2)

Tactic:
this.div_const 2

Premises used: HasSum.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
    (jacobiTheta τ - 1)
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    fun (i : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 * τ) * 2 / 2
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)

Tactic:
convert! this.div_const 2 using 1

Premises used: HasSum.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
    (jacobiTheta τ - 1)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    fun (i : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 * τ) * 2 / 2

Tactic:
simp_rw [mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Premises used: mul_div_cancel_right₀, two_ne_zero', Complex
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
rw : jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
rw₁ : jacobiTheta τ = 1 + (jacobiTheta τ - 1)
rw₂ : jacobiTheta τ = 1 + jacobiTheta τ - 1
rw₃ rw₄ : jacobiTheta τ = jacobiTheta τ
⊢ jacobiTheta τ =
    1 +
      HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))

Tactic:
rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
    add_sub_cancel_left]

Premises used: add_sub_assoc, hasSum_nat_jacobiTheta, add_sub_cancel_left, mul_div_cancel₀, HasSum.tsum_eq, two_ne_zero', Complex
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
rw :
  ‖HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
rw₁ :
  Norm.norm (E := ℂ) 2 *
      Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
rw₂ rw₃ :
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
⊢ ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))

Tactic:
rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]

Premises used: Iff.mpr, norm_mul, jacobiTheta_eq_tsum_nat, Complex.norm_two, sub_eq_iff_eq_add'
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
ha : LE.le (α := ℝ) 0 2
⊢ 2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
rw : 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
rw₁ rw₂ : rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2 = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
rw [div_mul_comm, mul_comm]

Premises used: div_mul_comm, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
τ₁ :
  ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
τ₂ :
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
τ₃ : 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]

Premises used: Real.pi, HMul.hMul, Complex.im, HSub.hSub, HDiv.hDiv, Real.exp, jacobiTheta, OfNat.ofNat, Neg.neg