awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₄ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * 1 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₅ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₆ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2)) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₇ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 / (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₈ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = 1 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₉ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₁₀ : jacobiTheta₂ 0 (-(↑τ : ℂ)⁻¹) = jacobiTheta₂ 0 (-1 / (↑τ : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 / (↑τ : ℂ))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₁₁ : jacobiTheta₂ 0 (-(↑τ : ℂ)⁻¹) = jacobiTheta₂ 0 (-(1 / (↑τ : ℂ)))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
have h : 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τ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
have refine_1 : ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ = y ^ HPow.hPow (β := ℕ) n 2
Tactic: refine (le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
refine_1 : ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ = y ^ HPow.hPow (β := ℕ) n 2
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
have refine_2 : y ^ HPow.hPow (β := ℕ) n 2 ≤ rexp (-π * τ.im) ^ n.natAbs
Tactic: refine (le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ = y ^ HPow.hPow (β := ℕ) n 2
have refine_1 : rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
Tactic: rw [norm_exp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) : ℂ) * (τ * I)
have push_cast : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ = (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ * I)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
have rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * -τ.im = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * τ : ℂ) = (π * n ^ 2 : ℝ) * (τ * I)),
        re_ofReal_mul, mul_I_re]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have this : ((↑π : ℂ) * 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this :
  ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = -π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1 : ∀ (m : ℕ) (hm : HPow.hPow (β := ℕ) n 2 = (↑m : ℤ)),
  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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 : ℤ)
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1 : rexp (-π * τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) = y ^ HPow.hPow (β := ℕ) n 2
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1₁ : rexp (-π * τ.im) ^ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 = y ^ HPow.hPow (β := ℕ) n 2
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1₂ : HPow.hPow (β := ℝ) (rexp (-π * τ.im)) (↑(HPow.hPow (β := ℕ) n 2) : ℝ) = y ^ HPow.hPow (β := ℕ) n 2
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1₃ : rexp (-π * τ.im) ^ HPow.hPow (β := ℕ) n 2 = y ^ HPow.hPow (β := ℕ) n 2
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1₄ : HPow.hPow (β := ℤ) (rexp (-π * τ.im)) (↑m : ℤ) = HPow.hPow (β := ℤ) y (↑m : ℤ)
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
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 : ℤ)
⊢ rexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ).re = y ^ HPow.hPow (β := ℕ) n 2
have refine_1₅ : rexp (-π * τ.im) ^ m = rexp (-π * τ.im) ^ m
Tactic: rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
have rw : HPow.hPow (β := ℕ) n 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑n.natAbs : ℤ) 2
Tactic: rw [Nat.cast_pow, Int.natAbs_sq]