awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
have step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
Tactic: have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by
    simp only [jacobiTheta₂_term_fderiv, smul_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul,
      mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term,
      jacobiTheta₂_term, mul_comm _ (cexp _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
    ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
have step1₁ : HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
Tactic: rw [funext step2] at step1
Cleared hypotheses: step1, step2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
have step3 : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ) z
Tactic: have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z :=
    (((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prodMk_left z τ)).hasDerivAt :)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 :
  HasSum (α := ℂ) (fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) = jacobiTheta₂'_term n z τ
step3 : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ) z
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
have rwa : ∀ (step3 : HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (∑' (b : ℤ), jacobiTheta₂'_term b z τ) z),
  HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
Tactic: rwa [← step1.tsum_eq] at step3
Cleared hypotheses: step3
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
have obtain : ∀ (T : ℝ) (hT : 0 < T) (hτ' : T < τ.im), ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
Tactic: obtain ⟨T, hT, hτ'⟩ := exists_between hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
have obtain : ∀ (S : ℝ) (hz : |z.im| < S), ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
Tactic: obtain ⟨S, hz⟩ := exists_gt |im z|
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
have hVo : IsOpen V
Tactic: have hVo : IsOpen V := ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _
    isOpen_Iio).prod (continuous_im.isOpen_preimage _ isOpen_Ioi)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) (z, τ)
have refine : ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V
Tactic: refine ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V
have refine_1 : ∀ (n : ℤ), ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2) V
Tactic: refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
refine_1 : ∀ (n : ℤ), ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2) V
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) V
have refine_2 : ∀ (n : ℤ) (x : ℂ × ℂ) (z' τ' : ℂ),
  (z', τ') ∈ V →
    ∀ (hz' : Membership.mem (γ := Set ℂ) {u : ℂ | |u.im| < S} (z', τ').1)
      (hτ' : Membership.mem (γ := Set ℂ) {v : ℂ | T < v.im} (z', τ').2),
      ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n
Tactic: refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
u : (n : ℤ) → ℝ :=
  fun (n : ℤ) ↦ 2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : Summable u
n : ℤ
⊢ ContinuousOn (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2) V
have refine_1 : Continuous (Y := ℂ) fun (p : ℂ × ℂ) ↦ jacobiTheta₂'_term n p.1 p.2
Tactic: apply Continuous.continuousOn
-- 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 : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [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
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
have rw : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
    cexp
      ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) =
  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 :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      cexp
        ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
have rw₁ : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
    (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
  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 :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      cexp
        ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
have rw₂ : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1) =
  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 :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      cexp
        ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) *
      (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) *
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) * 1) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
have rw₃ : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  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 : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (τ + 2)) =
    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 τ : ℂ
n : ℤ
⊢ (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
have push_cast : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (2 * (↑π : ℂ) * I)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
have rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
have rw₁ : cexp ((↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)) = 1
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
rw₁ : cexp ((↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)) = 1
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
have rw₂ : cexp (2 * (↑π : ℂ) * I) ^ HPow.hPow (β := ℕ) n 2 = 1
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
rw₁ : cexp ((↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)) = 1
rw₂ : cexp (2 * (↑π : ℂ) * I) ^ HPow.hPow (β := ℕ) n 2 = 1
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
have rw₃ : HPow.hPow (α := ℂ) 1 (HPow.hPow (β := ℕ) n 2) = 1
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
rw : (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2 = (↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)
rw₁ : cexp ((↑(HPow.hPow (β := ℕ) n 2) : ℂ) * (2 * (↑π : ℂ) * I)) = 1
rw₂ : cexp (2 * (↑π : ℂ) * I) ^ HPow.hPow (β := ℕ) n 2 = 1
rw₃ : HPow.hPow (α := ℂ) 1 (HPow.hPow (β := ℕ) n 2) = 1
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * 2) = 1
have rw₄ : Eq (α := ℂ) 1 1
Tactic: rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ
have refine : ∀ (n : ℤ), jacobiTheta₂_term n (z + 1) τ = 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 + 1) τ = jacobiTheta₂_term n z τ
have simp_rw : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
have simp_rw₁ : cexp
    (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
      (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
have simp_rw₂ : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * 1) *
    cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * 1) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
have simp_rw₃ : cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * 1) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₃ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
have simp_rw₄ : cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) *
    cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
n : ℤ
simp_rw :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (z + 1) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₁ :
  cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + 2 * (↑π : ℂ) * I * (↑n : ℂ) * 1 +
        (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₂ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * 1) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₃ :
  cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp (2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
simp_rw₄ :
  cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) *
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
    cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
⊢ jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
have simp_rw₅ : cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * 1 * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ) =
  cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I) * z) * cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]