Differentiable At jacobi Theta₂ half

lemma differentiableAt_jacobiTheta₂_half (τ : ℍ) :    DifferentiableAt ℂ (fun t : ℂ => jacobiTheta₂ (t / 2) t) ↑τ := by  let f : ℂ → ℂ × ℂ := fun t => (t / 2, t)  have hf : DifferentiableAt ℂ f ↑τ :=    (differentiableAt_id.mul_const ((2 : ℂ)⁻¹)).prodMk differentiableAt_id  have hg : DifferentiableAt ℂ (fun p : ℂ × ℂ => jacobiTheta₂ p.1 p.2) (f ↑τ) := by    simpa [f] using (hasFDerivAt_jacobiTheta₂ ((τ : ℂ) / 2) τ.2).differentiableAt  change DifferentiableAt ℂ (((fun p : ℂ × ℂ => jacobiTheta₂ p.1 p.2) ∘ f)) ↑τ  exact DifferentiableAt.comp (x := (τ : ℂ)) hg hf