-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) :
    π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Proof state:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
refine le_trans ?_ this

Result:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖

Proof state:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖

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]

Result:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (π * ↑|n| ^ 2) ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖)

Proof state:
n : ℤ
z τ : ℂ
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖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]

Result:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Proof state:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * ‖(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]

Result:
no goals

Proof state:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (π * ↑|n| ^ 2) ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖)

Tactic:
refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)

Result:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = ‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖

Proof state:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = ‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖

Tactic:
simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
  Int.cast_abs, ← norm_intCast, norm_pow]

Result:
no goals

Proof state:
n : ℤ
z τ : ℂ
⊢ ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
refine (ContinuousLinearMap.le_opNorm _ _).trans ?_

Result:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * ‖(0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖