awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
_ :
  ∑' (n : ℤ), cexp (-(↑π : ℂ) * (-I * τ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * (I * z) * (↑n : ℂ)) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2)
_₁ :
  1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / (-I * τ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * (I * z)) 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
_₂ :
  1 / (-I * τ) ^ (1 / 2) * cexp ((↑π : ℂ) * I * (-1 / τ) * HPow.hPow (β := ℕ) z 2) *
      ∑' (n : ℤ),
        cexp
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))
⊢ ∑' (n : ℤ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      ∑' (n : ℤ),
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z / τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (-1 / τ))

Tactic:
calc
  _ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) :=
    tsum_congr (fun n ↦ by ring_nf)
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
    rw [tsum_exp_neg_quadratic h2]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) := by
    simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
    congr 2 with n : 1; congr 1
    field_simp
    ring_nf
    simp_rw [I_sq, I_pow_four]
    ring_nf
  _ = _ := by
    congr 3
    ring

Premises used: Real.pi, HMul.hMul, tsum_congr, HDiv.hDiv, Complex.ofReal, HPow.hPow, HAdd.hAdd, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂' z τ =
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
inr :
  ∀ (hτ : 0 < τ.im),
    jacobiTheta₂' z τ =
      1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rcases le_or_gt (im τ) 0 with hτ | hτ

Premises used: Complex.im, le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl inl₁ : (-1 / τ).im ≤ 0
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [jacobiTheta₂'_undef z hτ, jacobiTheta₂'_undef, jacobiTheta₂_undef, mul_zero,
      sub_zero, mul_zero]

Premises used: sub_zero, MulZeroClass.mul_zero, jacobiTheta₂_undef, jacobiTheta₂'_undef
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl : 0 ≤ HDiv.hDiv (β := ℝ) (-τ.im) ((normSq : (a : ℂ) → ℝ) τ : ℝ)
⊢ (-1 / τ).im ≤ 0

Tactic:
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Premises used: neg_div, neg_nonpos, one_div, Complex.inv_im, Complex.neg_im
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
rw : 0 < HDiv.hDiv (β := ℝ) τ.im ((normSq : (a : ℂ) → ℝ) τ : ℝ)
⊢ 0 < (-1 / τ).im

Tactic:
rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]

Premises used: neg_div, neg_one_mul, neg_neg, div_eq_mul_inv, Complex.inv_im, Complex.neg_im
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < HDiv.hDiv (β := ℝ) τ.im ((normSq : (a : ℂ) → ℝ) τ : ℝ)

Tactic:
div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))

Premises used: Iff.mpr, Complex.normSq_pos, lt_irrefl, div_pos, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < HDiv.hDiv (β := ℝ) τ.im ((normSq : (a : ℂ) → ℝ) τ : ℝ)

Tactic:
exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))

Premises used: Iff.mpr, Complex.normSq_pos, lt_irrefl, div_pos, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 / τ).im

Tactic:
have hτ' : 0 < (-1 / τ).im := by
    rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]
    exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x (-1 / τ)) (jacobiTheta₂' (z / τ) (-1 / τ)) (z / τ)

Tactic:
have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
this : HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x (-1 / τ)) (jacobiTheta₂' (z / τ) (-1 / τ)) (z / τ)
⊢ HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z

Tactic:
simpa only [mul_comm, one_div] using this.comp z (hasDerivAt_mul_const τ⁻¹)

Premises used: HasDerivAt.comp, Inv.inv, one_div, mul_comm, hasDerivAt_mul_const
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
⊢ HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z

Tactic:
have hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ))
      ((1 / τ) * jacobiTheta₂' (z / τ) (-1 / τ)) z := by
    have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'
    simpa only [mul_comm, one_div] using this.comp z (hasDerivAt_mul_const τ⁻¹)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ jacobiTheta₂' z τ = deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z

Tactic:
(hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm

Premises used: HasDerivAt.deriv, hasDerivAt_jacobiTheta₂_fst, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
rw rw₁ :
  Eq (α := ℂ)
    (deriv
      (fun (x : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) x 2 / τ) * jacobiTheta₂ (x / τ) (-1 / τ))
      z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
⊢ Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)

Tactic:
rw [funext (jacobiTheta₂_functional_equation · τ)]

Premises used: jacobiTheta₂_functional_equation, funext
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
simp_rw :
  deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * (cexp (-(↑π : ℂ) * (I * HPow.hPow (β := ℕ) z 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ)))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * (I * HPow.hPow (β := ℕ) z 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
⊢ deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
simp_rw [mul_assoc, deriv_const_mul_field]

Premises used: mul_assoc, deriv_const_mul_field
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
rw : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)

Tactic:
rw [deriv_fun_mul _ hj.differentiableAt]

Premises used: deriv_fun_mul, HasDerivAt.differentiableAt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z

Tactic:
(((differentiableAt_pow 2).const_mul _).mul_const _).cexp

Premises used: DifferentiableAt.const_mul, DivInvMonoid.div', DifferentiableAt.mul_const, DifferentiableAt.cexp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z

Tactic:
exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp

Premises used: DifferentiableAt.const_mul, DifferentiableAt.mul_const, DifferentiableAt.cexp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
rw :
  1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [hj.deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
rw :
  (cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) *
            (-(↑π : ℂ) * I * ((↑2 : ℂ) * z ^ HSub.hSub (α := ℕ) 2 1) * τ⁻¹) *
          jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹)) z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]

Premises used: deriv_mul_const_field, deriv_const_mul_field, deriv_cexp, deriv_pow_field, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) *
            (-(↑π : ℂ) * I * ((↑2 : ℂ) * z ^ HSub.hSub (α := ℕ) 2 1) * τ⁻¹) *
          jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun (w : ℂ) ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
_ :
  Eq (α := ℂ) (deriv (fun (x : ℂ) ↦ jacobiTheta₂ x τ) z)
    (deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z)
_₁ :
  deriv
      (fun (z : ℂ) ↦
        1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ))
      z =
    1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
_₂ :
  1 / (-I * τ) ^ (1 / 2) *
      deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)
_₃ :
  1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun (z : ℂ) ↦ cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) * deriv (fun (z : ℂ) ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf

Premises used: Real.pi, HMul.hMul, deriv, HasDerivAt.deriv, hasDerivAt_jacobiTheta₂_fst, jacobiTheta₂, HDiv.hDiv, Complex.ofReal, HPow.hPow, HAdd.hAdd, Complex.exp, OfNat.ofNat, Eq.symm, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom :
  ‖denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1
⊢ SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k

Tactic:
have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom :
  ‖denom
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑τ : ℂ)‖ ≤
    1
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) (γ • τ) : ℂ)

Tactic:
simpa only [slash_action_eqn_SL'' _ (mem_Gamma_one γ), norm_mul, norm_zpow]
      using le_mul_of_one_le_left (norm_nonneg _) <|
        one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk

Premises used: Iff.mpr, norm_pos_iff, CongruenceSubgroup.mem_Gamma_one, le_mul_of_one_le_left, norm_mul, one_le_zpow_of_nonpos₀, SlashInvariantForm.slash_action_eqn_SL'', norm_zpow, norm_nonneg, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
⊢ SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k

Tactic:
have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ (f : (a : ℍ) → ℂ) (S • UpperHalfPlane.I) =
    HMul.hMul (β := ℂ)
      (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
          (↑UpperHalfPlane.I : ℂ) ^
        k)
      ((f : (a : ℍ) → ℂ) UpperHalfPlane.I : ℂ)

Tactic:
have hI := slash_action_eqn_SL'' f (mem_Gamma_one S) I
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  (f : (a : ℍ) → ℂ) (S • UpperHalfPlane.I) =
    HMul.hMul (β := ℂ)
      (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
          (↑UpperHalfPlane.I : ℂ) ^
        k)
      ((f : (a : ℍ) → ℂ) UpperHalfPlane.I : ℂ)
⊢ (f : (a : ℍ) → ℂ)
      (S • HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) =
    HMul.hMul (β := ℂ)
      (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
          (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^
        k)
      ((f : (a : ℍ) → ℂ)
          (HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) :
        ℂ)

Tactic:
have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ((⟨2, two_pos⟩ : {x : ℝ // 0 < x}) • .I)
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this_1 : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = (↑UpperHalfPlane.I : ℂ) ^ k * c
h2I2 :
  c =
    (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^ k * c
this : HPow.hPow (α := ℂ) 2 k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0

Tactic:
simpa [mul_zpow, zpow_ne_zero, this] using h2I2.symm.trans hI

Premises used: mul_zpow, zpow_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = (↑UpperHalfPlane.I : ℂ) ^ k * c
h2I2 :
  c =
    (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^ k * c
suffices : HPow.hPow (α := ℂ) 2 k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0

Tactic:
suffices (2 : ℂ) ^ k = 1 ↔ k = 0 by
    simpa [mul_zpow, zpow_ne_zero, this] using h2I2.symm.trans hI
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = (↑UpperHalfPlane.I : ℂ) ^ k * c
h2I2 :
  c =
    (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^ k * c
⊢ Ne (α := ℝ) 2 1

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
f : F
c : ℂ
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = (↑UpperHalfPlane.I : ℂ) ^ k * c
h2I2 :
  c =
    (↑(HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) 2 ⋯) UpperHalfPlane.I) : ℂ) ^ k * c
⊢ HPow.hPow (α := ℂ) 2 k = 1 ↔ k = 0

Tactic:
simpa using ofReal_inj.trans <| zpow_eq_one_iff_right₀ (two_pos.le : (0 : ℝ) ≤ 2) (by norm_num1)

Premises used: two_pos, LT.lt.le, zpow_eq_one_iff_right₀, Iff.trans, Complex.ofReal_inj