-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma hasSum_qExpansion_of_abs_lt [NeZero n] [ModularFormClass F Γ(n) k]
    {q : ℂ} (hq : ‖q‖ < 1) :
    HasSum (fun m : ℕ ↦ (qExpansion n f).coeff ℂ m • q ^ m) (cuspFunction n f q)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Tactic:
have hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1) := by
  refine fun z hz ↦ (differentiableAt_cuspFunction n f ?_).differentiableWithinAt
  simpa using hz

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖z‖ < 1

Tactic:
simpa using hz

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
⊢ DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)

Tactic:
refine fun z hz ↦ (differentiableAt_cuspFunction n f ?_).differentiableWithinAt

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖z‖ < 1

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
⊢ q ∈ Metric.ball 0 1

Tactic:
simpa using hq

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
⊢ HasSum (fun m => (PowerSeries.coeff ℂ m) (qExpansion n f) • q ^ m) (cuspFunction n f q)

Tactic:
simp only [qExpansion_coeff, ← eq_cuspFunction n f]

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Proof state:
case h.e'_5.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
qmem : q ∈ Metric.ball 0 1
m : ℕ
⊢ ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m =
    (↑m.factorial)⁻¹ • (q - 0) ^ m • iteratedDeriv m (cuspFunction n f) 0

Tactic:
rw [sub_zero, smul_eq_mul, smul_eq_mul, mul_right_comm, smul_eq_mul, mul_assoc]

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Tactic:
have qmem : q ∈ Metric.ball 0 1 := by simpa using hq

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
qmem : q ∈ Metric.ball 0 1
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
qmem : q ∈ Metric.ball 0 1
⊢ HasSum (fun m => ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m) (cuspFunction n f q)

Tactic:
convert hasSum_taylorSeries_on_ball hdiff qmem using 2 with m

Result:
case h.e'_5.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1)
qmem : q ∈ Metric.ball 0 1
m : ℕ
⊢ ((↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0) • q ^ m =
    (↑m.factorial)⁻¹ • (q - 0) ^ m • iteratedDeriv m (cuspFunction n f) 0