-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
    HasDerivAt (jacobiTheta₂ · τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0))
    ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
  apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)

Result:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z

Tactic:
exact ((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prod_mk_left z τ)).hasDerivAt

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
rw [funext step2] at step1

Result:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
step3 : HasDerivAt (fun x => jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
rwa [← step1.tsum_eq] at step3

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (m : ℂ) (x : ℂ × ℂ →L[ℂ] ℂ),
    { toFun := fun f => f (1, 0), map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id ℂ) m • { toFun := fun f => f (1, 0), map_add' := ⋯ }.toFun x

Tactic:
simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul,
RingHom.id_apply, forall_const]

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (x y : ℂ × ℂ →L[ℂ] ℂ), (fun f => f (1, 0)) (x + y) = (fun f => f (1, 0)) x + (fun f => f (1, 0)) y

Tactic:
simp only [ContinuousLinearMap.add_apply, forall_const]

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
let eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
{ toFun := fun f ↦ f (1, 0)
  cont := continuous_id'.clm_apply continuous_const
  map_add' := by simp only [ContinuousLinearMap.add_apply, forall_const]
  map_smul' := by simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul,
    RingHom.id_apply, forall_const] }

Result:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z := by
  exact ((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prod_mk_left z τ)).hasDerivAt

Result:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
step3 : HasDerivAt (fun x => jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
n : ℤ
⊢ (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
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 _)]

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) 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 _)]

Result:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
⊢ HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Proof state:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))

Tactic:
apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)

Result:
no goals