awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
refine_1 :
  ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ)‖ ≤
    2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
          HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
            (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 + 1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2)
have refine_2 : ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
      (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
  1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
Tactic: refine mul_le_mul_of_nonneg_left ((norm_add_le _ _).trans (add_le_add ?_ ?_)) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ)‖ ≤
    2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
have refine_1 : 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
  2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
Tactic: simp_rw [hns, norm_mul, ← ofReal_ofNat, ← ofReal_intCast,
      norm_real, norm_of_nonneg zero_le_two, Real.norm_of_nonneg pi_pos.le, norm_I, mul_one,
      Real.norm_eq_abs, ← Int.cast_abs, ← Int.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
have h₁ : 0 ≤ 2 * π * (↑|n| : ℝ)
Tactic: grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
h₁ : 0 ≤ 2 * π * (↑|n| : ℝ)
⊢ 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
have refine_1 : 2 * π * (↑|n| : ℝ) * 1 ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
Tactic: grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
h₁ : 0 ≤ 2 * π * (↑|n| : ℝ)
refine_1 : 2 * π * (↑|n| : ℝ) * 1 ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
⊢ 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
have refine_1₁ : 2 * π * (↑|n| : ℝ) ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
Tactic: grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
h₁ : 0 ≤ 2 * π * (↑|n| : ℝ)
refine_1 : 2 * π * (↑|n| : ℝ) * 1 ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
refine_1₁ : 2 * π * (↑|n| : ℝ) ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
⊢ 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
have refine_1₂ : 2 * π * (↑|n| : ℝ) ≤ 2 * π * (↑|n| : ℝ)
Tactic: grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
have refine_2 : π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤
  π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2
Tactic: simp_rw [hns, norm_mul, one_mul, norm_I, mul_one,
      norm_real, norm_of_nonneg pi_pos.le, ← ofReal_intCast, ← ofReal_pow, norm_real,
      Real.norm_eq_abs, Int.cast_abs, abs_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤
    π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2
have refine_2 : Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤ 1
Tactic: apply mul_le_of_le_one_right (mul_nonneg pi_pos.le (pow_nonneg (abs_nonneg _) _))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
⊢ Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have refine : ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have simp_rw : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
simp_rw :
  ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤
    ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have simp_rw₁ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
simp_rw :
  ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤
    ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₁ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have simp_rw₂ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max 0 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
simp_rw :
  ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤
    ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₁ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₂ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max 0 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have simp_rw₃ : ‖jacobiTheta₂_term_fderiv n z τ‖ * 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
simp_rw :
  ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤
    ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₁ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₂ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max 0 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₃ : ‖jacobiTheta₂_term_fderiv n z τ‖ * 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have simp_rw₄ : ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
n : ℤ
z τ : ℂ
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have this : Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: have : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖ := by
    refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
    simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have refine : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ)
Tactic: refine le_trans ?_ this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ)
have simp_rw : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
    (π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2) ≤
  ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
    (‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖)
Tactic: simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, ContinuousLinearMap.coe_smul',
    Pi.smul_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul',
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply, smul_zero, zero_add,
    smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2) ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖)
have refine : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw₂ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * 1 * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₂ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * 1 * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw₃ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₂ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * 1 * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₃ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw₄ : π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₂ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * 1 * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₃ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₄ : π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
have simp_rw₅ : π * HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) (↑n : ℂ)) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
Tactic: simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im
have mp : (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
mp : (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im
⊢ (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im
have mpr : 0 < τ.im → Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im
have mp : (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) →
  Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
Tactic: rw [← summable_jacobiTheta₂_term_iff (z := z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
have this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
Tactic: have := h.norm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
have mp : ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖
Tactic: refine this.of_norm_bounded_eventually ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖
have this₁ : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
Tactic: have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖
have h₁ : ∀ (n : ℤ) (hn : n ≠ 0), ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Tactic: filter_upwards [this] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
have h₁ : ‖jacobiTheta₂_term n z τ‖ ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖
Tactic: refine le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖
have h₁ : 1 ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
Tactic: apply le_mul_of_one_le_left (norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
have h₁ : 2⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
Tactic: refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 2⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
have h₁ : 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
Tactic: refine (by norm_num : 2⁻¹ ≤ (1 : ℝ)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
have h₁ : 1 ≤ |n|
Tactic: rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
have mpr : ∀ (n : ℤ),
  ‖jacobiTheta₂_term_fderiv n z τ‖ ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
Tactic: refine ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 2).mul_left (3 * π)).of_norm_bounded (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
have mpr : 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
  3 * π *
    (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
Tactic: refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
have mpr : 3 * π * (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖) ≤
  3 * π *
    (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
Tactic: simp_rw [mul_assoc (3 * π)]