-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem hasSum_nat_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
    HasSum (fun n : ℕ => cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
have := hasSum_jacobiTheta₂_term 0 hτ

Result:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun n => jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Proof state:
case h.e'_5
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)
⊢ (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) = fun i => cexp (↑π * I * (↑i + 1) ^ 2 * τ) * 2 / 2

Tactic:
simp_rw [mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
convert this.div_const 2 using 1

Result:
case h.e'_5
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)
⊢ (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) = fun i => cexp (↑π * I * (↑i + 1) ^ 2 * τ) * 2 / 2

Proof state:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n => cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + (1 - 1 * 2))
⊢ 1 - 1 * 2 = -1

Tactic:
norm_num

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
have := this.nat_add_neg

Result:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n => cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Proof state:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n => cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
  Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
  Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ← sub_eq_add_neg,
  Nat.cast_add, Nat.cast_one] at this

Result:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun n => jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this

Result:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Proof state:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n => cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
rw [← hasSum_nat_add_iff' 1] at this

Result:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n => cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)