awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
| cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂ z τ
have rw : ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ
Tactic: rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂ z τ
have conv_rhs : jacobiTheta₂ (z + τ) τ =
  ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ
Tactic: conv_rhs => rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ =
    ∑' (c : ℤ), cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) c) z τ
have refine : ∀ (n : ℤ),
  jacobiTheta₂_term n (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) n) z τ
Tactic: refine tsum_congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1 : (a : ℤ) → ℤ) n) z τ
have simp_rw : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp
    (-(↑π : ℂ) * I * (τ + 2 * z) +
      (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ) * z +
        (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ)) 2 * τ))
Tactic: simp_rw [jacobiTheta₂_term, ← Complex.exp_add, Equiv.coe_addRight, Int.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
| jacobiTheta₂ (-z) τ
have rw : ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ
Tactic: rw [jacobiTheta₂, ← Equiv.tsum_eq (Equiv.neg ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ
have conv_lhs : ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ = jacobiTheta₂ z τ
Tactic: conv_lhs => rw [jacobiTheta₂, ← Equiv.tsum_eq (Equiv.neg ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) c) (-z) τ = jacobiTheta₂ z τ
have refine : ∀ (n : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
Tactic: refine tsum_congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
have simp_rw : cexp
    (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
      (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp
      (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
have simp_rw₁ : cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp
      (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
have simp_rw₂ : cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (-(↑n : ℂ)) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp
      (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (-(↑n : ℂ)) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
have simp_rw₃ : cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp
      (2 * (↑π : ℂ) * I * (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) * -z +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑((Equiv.neg ℤ : (a : ℤ) → ℤ) n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑(-n) : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-n) : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (-(↑n : ℂ)) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₃ :
  cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * -z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term ((Equiv.neg ℤ : (a : ℤ) → ℤ) n) (-z) τ = jacobiTheta₂_term n z τ
have simp_rw₄ : cexp (2 * ((↑π : ℂ) * (I * (-(↑n : ℂ) * -z))) + (↑π : ℂ) * (I * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))) =
  cexp (2 * ((↑π : ℂ) * (I * ((↑n : ℂ) * z))) + (↑π : ℂ) * (I * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)))
Tactic: simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂ z τ) =
    jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
have rw : ∑' (a : ℤ), (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term a (-z) τ) =
  jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
Tactic: rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term a (-z) τ) =
    jacobiTheta₂ ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
have e_f : ∀ (n : ℤ),
  (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂_term n (-z) τ) =
    jacobiTheta₂_term n ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)
Tactic: congr 2 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ
have refine : ∀ (n : ℤ), jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ
Tactic: refine tsum_congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ
have simp_rw : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
Tactic: simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have rw : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      cexp
        ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
Tactic: rw [mul_add, Complex.exp_add, this, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp
          ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have rw₁ : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2))) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
Tactic: rw [mul_add, Complex.exp_add, this, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp
          ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₁ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have rw₂ : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1)) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
Tactic: rw [mul_add, Complex.exp_add, this, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
this : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
rw :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp
          ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₁ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
rw₂ :
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have rw₃ : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
Tactic: rw [mul_add, Complex.exp_add, this, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2))) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have suffices : cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
Tactic: suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
    (∑' (n : ℤ),
      2 * (↑π : ℂ) * I * (↑n : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ))
have refine : ∀ (n : ℤ),
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: refine tsum_congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inl : ∀ (hτ : τ.im ≤ 0),
  jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
Tactic: rcases le_or_gt τ.im 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
inl :
  ∀ (hτ : τ.im ≤ 0),
    jacobiTheta₂' (z + τ) τ =
      cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inr : ∀ (hτ : 0 < τ.im),
  jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
Tactic: rcases le_or_gt τ.im 0 with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inl : jacobiTheta₂' (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * 0)
Tactic: simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl : jacobiTheta₂' (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * 0)
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inl₁ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (0 - 2 * (↑π : ℂ) * I * 0)
Tactic: simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl : jacobiTheta₂' (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * 0)
inl₁ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (0 - 2 * (↑π : ℂ) * I * 0)
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inl₂ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * HSub.hSub (α := ℂ) 0 0
Tactic: simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
inl : jacobiTheta₂' (z + τ) τ = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * 0)
inl₁ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (0 - 2 * (↑π : ℂ) * I * 0)
inl₂ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * HSub.hSub (α := ℂ) 0 0
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have inl₃ : 0 = cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * 0
Tactic: simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
| cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
    (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) *
        cexp (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ) -
      2 * (↑π : ℂ) * I *
        cexp (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ))
have rw : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
  cexp
    ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
        (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
      -(↑π : ℂ) * I * (τ + 2 * z))
Tactic: rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
      mul_add, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
      (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) *
          cexp
            (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ) -
        2 * (↑π : ℂ) * I *
          cexp
            (2 * (↑π : ℂ) * I * (↑(n + 1) : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(n + 1) : ℂ) 2 * τ))
have conv_rhs : 2 * (↑π : ℂ) * I * (↑n : ℂ) *
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  2 * (↑π : ℂ) * I * (↑n : ℂ) *
    cexp
      ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
          (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
        -(↑π : ℂ) * I * (τ + 2 * z))
Tactic: conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
      mul_add, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        ((2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
            (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
          -(↑π : ℂ) * I * (τ + 2 * z))
have e_a : 2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + τ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
  (2 * (↑π : ℂ) * I * (↑n : ℂ) + 2 * (↑π : ℂ) * I) * z +
      (↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ +
    -(↑π : ℂ) * I * (τ + 2 * z)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ z τ)
have this : ∀ (n : ℤ),
  jacobiTheta₂'_term n (z + τ) τ =
    cexp (-(↑π : ℂ) * I * (τ + 2 * z)) *
      (jacobiTheta₂'_term (n + 1) z τ - 2 * (↑π : ℂ) * I * jacobiTheta₂_term (n + 1) z τ)
Tactic: have (n : ℤ) : jacobiTheta₂'_term n (z + τ) τ =
      cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ -
      2 * π * I * jacobiTheta₂_term (n + 1) z τ) := by
    simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
    conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
      mul_add, mul_one, add_sub_cancel_right]
    congr 2
    ring