-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma qExpansionFormalMultilinearSeries_radius [NeZero n] [ModularFormClass F Γ(n) k] :
    1 ≤ (qExpansionFormalMultilinearSeries n f).radius

Proof state:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f)‖ * |↑r| ^ n_1

Tactic:
simp_rw [← Real.norm_eq_abs, ← Complex.norm_real, ← norm_pow, ← norm_mul]

Result:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f) * ↑↑r ^ n_1‖

Proof state:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f) * ↑↑r ^ n_1‖

Tactic:
exact (hasSum_qExpansion_of_abs_lt n f (q := r) (by simpa using hr)).summable.norm

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ ‖↑↑r‖ < 1

Tactic:
simpa using hr

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
⊢ 1 ≤ (qExpansionFormalMultilinearSeries n f).radius

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : ENNReal
hr : r < 1
⊢ r ≤ (qExpansionFormalMultilinearSeries n f).radius

Proof state:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f)‖ * ↑r ^ n_1

Tactic:
rw [← r.abs_eq]

Result:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f)‖ * |↑r| ^ n_1

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : ENNReal
hr : r < 1
⊢ r ≤ (qExpansionFormalMultilinearSeries n f).radius

Tactic:
lift r to NNReal using hr.ne_top

Result:
case intro
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ ↑r ≤ (qExpansionFormalMultilinearSeries n f).radius

Proof state:
case intro
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ ↑r ≤ (qExpansionFormalMultilinearSeries n f).radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_summable

Result:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖qExpansionFormalMultilinearSeries n f n_1‖ * ↑r ^ n_1

Proof state:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖qExpansionFormalMultilinearSeries n f n_1‖ * ↑r ^ n_1

Tactic:
simp only [qExpansionFormalMultilinearSeries_apply_norm]

Result:
case intro.h
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
r : NNReal
hr : ↑r < 1
⊢ Summable fun n_1 => ‖(PowerSeries.coeff ℂ n_1) (qExpansion n f)‖ * ↑r ^ n_1