awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
⊢ 0 < (w + (↑h : ℂ)).im

Tactic:
have : 0 < im (w + h) := by simp [hw]
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
pos :
  Eq (α := ℂ) ((f : (a : ℍ) → ℂ) { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ)
    ((f : (a : ℍ) → ℂ) { coe := w, coe_im_pos := hw : ℍ } : ℂ)
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)

Tactic:
simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, Function.comp_apply
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ { coe := w, coe_im_pos := hw : ℍ }) : ℂ)
    ((f : (a : ℍ) → ℂ) { coe := w, coe_im_pos := hw : ℍ } : ℂ)

Tactic:
SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ

Premises used: UpperHalfPlane.mk, SlashInvariantForm.vAdd_apply_of_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
h₁ : { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } = h +ᵥ { coe := w, coe_im_pos := hw : ℍ }
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ)
    ((f : (a : ℍ) → ℂ) { coe := w, coe_im_pos := hw : ℍ } : ℂ)

Tactic:
convert! SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ using 2

Premises used: UpperHalfPlane.mk, SlashInvariantForm.vAdd_apply_of_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
h₁ : (↑{ coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ) = (↑(h +ᵥ { coe := w, coe_im_pos := hw : ℍ }) : ℂ)
⊢ { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } = h +ᵥ { coe := w, coe_im_pos := hw : ℍ }

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
⊢ (↑{ coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ) = (↑(h +ᵥ { coe := w, coe_im_pos := hw : ℍ }) : ℂ)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ (w + (↑h : ℂ)).im ≤ 0

Tactic:
simpa using hw
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ (w + (↑h : ℂ)).im ≤ 0

Tactic:
have : im (w + h) ≤ 0 := by simpa using hw
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
this : (w + (↑h : ℂ)).im ≤ 0
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)

Tactic:
simp [ofComplex_apply_of_im_nonpos this, ofComplex_apply_of_im_nonpos hw]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_nonpos
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
τ : ℍ
hΓ : h ∈ Γ.strictPeriods
hh : h ≠ 0
⊢ cuspFunction h (⇑f : (a : ℍ) → ℂ) (𝕢 h (↑τ : ℂ)) = (f : (a : ℍ) → ℂ) τ

Tactic:
eq_cuspFunction τ hh (SlashInvariantFormClass.periodic_comp_ofComplex f hΓ)

Premises used: UpperHalfPlane.eq_cuspFunction, SlashInvariantFormClass.periodic_comp_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst_1 : ModularFormClass F Γ k
hi : IsCusp OnePoint.infty Γ
⊢ I∞.BoundedAtFilter (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))

Tactic:
(OnePoint.isBoundedAt_infty_iff.mp (bdd_at_cusps f hi)).comp_tendsto tendsto_comap_im_ofComplex

Premises used: Filter.BoundedAtFilter, OnePoint.isBoundedAt_infty_iff, Iff.mp, ModularFormClass.bdd_at_cusps, Asymptotics.IsBigO.comp_tendsto, UpperHalfPlane.tendsto_comap_im_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : ModularFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
q : ℂ
hq : ‖q‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) q

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
  differentiableAt_cuspFunction hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) hq

Premises used: SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, Fact.mk, UpperHalfPlane.differentiableAt_cuspFunction, Subgroup.isCusp_of_mem_strictPeriods, ModularFormClass.holo
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : ModularFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
⊢ AnalyticAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) 0

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
  analyticAt_cuspFunction_zero hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f)

Premises used: SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, Fact.mk, UpperHalfPlane.analyticAt_cuspFunction_zero, Subgroup.isCusp_of_mem_strictPeriods, ModularFormClass.holo
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
m : ℕ
⊢ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0

Tactic:
simp [qExpansion]

Premises used: UpperHalfPlane.qExpansion
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ (PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) = valueAtInfty f

Tactic:
simp [qExpansion_coeff, cuspFunction_apply_zero hh hfanalytic hfper]

Premises used: UpperHalfPlane.qExpansion_coeff, UpperHalfPlane.cuspFunction_apply_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ Membership.mem (γ := Set ℂ) (ball 0 1) q

Tactic:
simpa using hq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
h₁ :
  ∀ (m : ℕ),
    HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (q ^ m) =
      HSMul.hSMul (α := ℂ) (↑m.factorial : ℂ)⁻¹ ((q - 0) ^ m • iteratedDeriv m (cuspFunction h f) 0)
⊢ HasSum
    (fun (m : ℕ) ↦ HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (q ^ m))
    (cuspFunction h f q)

Tactic:
convert!
    hasSum_taylorSeries_on_ball (differentiableOn_cuspFunction_ball hh hfper hfhol hfbdd)
      (by simpa using hq) using
    2 with m

Premises used: Complex.hasSum_taylorSeries_on_ball, UpperHalfPlane.differentiableOn_cuspFunction_ball
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
m : ℕ
⊢ HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (q ^ m) =
    HSMul.hSMul (α := ℂ) (↑m.factorial : ℂ)⁻¹ ((q - 0) ^ m • iteratedDeriv m (cuspFunction h f) 0)

Tactic:
grind [qExpansion_coeff, sub_zero, smul_eq_mul]

Premises used: sub_zero, UpperHalfPlane.qExpansion_coeff, smul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
⊢ 0 < 2 * π * τ.im / h

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
⊢ 0 < 2 * π * τ.im / h

Tactic:
have : 0 < 2 * π * τ.im / h := by positivity
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this : 0 < 2 * π * τ.im / h
⊢ ‖𝕢 h (↑τ : ℂ)‖ < 1

Tactic:
simpa [Periodic.qParam, Complex.norm_exp, neg_div]

Premises used: Function.Periodic.qParam, neg_div, Complex.norm_exp
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this : 0 < 2 * π * τ.im / h
⊢ ‖𝕢 h (↑τ : ℂ)‖ < 1

Tactic:
have : ‖𝕢 h τ‖ < 1 := by simpa [Periodic.qParam, Complex.norm_exp, neg_div]
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this_1 : 0 < 2 * π * τ.im / h
this : ‖𝕢 h (↑τ : ℂ)‖ < 1
⊢ HasSum
    (fun (m : ℕ) ↦
      HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (𝕢 h (↑τ : ℂ) ^ m))
    (f τ)

Tactic:
simpa [eq_cuspFunction τ hh.ne' hfper] using
    hasSum_qExpansion_of_norm_lt hh hfper hfhol hfbdd this

Premises used: UpperHalfPlane.eq_cuspFunction, LT.lt.ne', UpperHalfPlane.hasSum_qExpansion_of_norm_lt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ (qExpansionFormalMultilinearSeries h f).coeff m =
    (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))

Tactic:
simp [qExpansionFormalMultilinearSeries, FormalMultilinearSeries.coeff_ofScalars]

Premises used: FormalMultilinearSeries.coeff_ofScalars, UpperHalfPlane.qExpansionFormalMultilinearSeries
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
rw :
  norm (E := ℂ)
      ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ) :
            (a : ContinuousMultilinearMap ℂ (fun (x : Fin m) ↦ ℂ) ℂ) → ℂ)
          (FormalMultilinearSeries.ofScalars ℂ
            (fun (m : ℕ) ↦ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))) m) :
        ℂ) =
    norm (E := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
⊢ ‖qExpansionFormalMultilinearSeries h f m‖ =
    norm (E := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)

Tactic:
rw [qExpansionFormalMultilinearSeries,
    ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, UpperHalfPlane.qExpansionFormalMultilinearSeries, ContinuousMultilinearMap.piFieldEquiv, Complex, Fin
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ norm (E := ℂ)
      ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ) :
            (a : ContinuousMultilinearMap ℂ (fun (x : Fin m) ↦ ℂ) ℂ) → ℂ)
          (FormalMultilinearSeries.ofScalars ℂ
            (fun (m : ℕ) ↦ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))) m) :
        ℂ) =
    norm (E := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ 1 ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
refine : ∀ (r : ENNReal) (hr : r < 1), r ≤ (qExpansionFormalMultilinearSeries h f).radius
⊢ 1 ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : ENNReal
hr : r < 1
⊢ r ≠ ⊤

Tactic:
hr.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : ENNReal
hr : r < 1
lift : ∀ (r : NNReal) (hr : (↑r : ENNReal) < 1), (↑r : ENNReal) ≤ (qExpansionFormalMultilinearSeries h f).radius
⊢ r ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
lift r to NNReal using hr.ne_top

Premises used: LT.lt.ne_top, NNReal
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
h₁ : Summable (α := ℝ) fun (n : ℕ) ↦ ‖qExpansionFormalMultilinearSeries h f n‖ * (↑r : ℝ) ^ n
⊢ (↑r : ENNReal) ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_summable

Premises used: FormalMultilinearSeries.le_radius_of_summable
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
h₁ :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) * (↑r : ℝ) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖qExpansionFormalMultilinearSeries h f n‖ * (↑r : ℝ) ^ n

Tactic:
simp only [qExpansionFormalMultilinearSeries_apply_norm]

Premises used: UpperHalfPlane.qExpansionFormalMultilinearSeries_apply_norm
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
h₁ :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) *
      |(↑r : ℝ)| ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) * (↑r : ℝ) ^ n

Tactic:
rw [← r.abs_eq]

Premises used: NNReal.abs_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
h₁ :
  Summable (α := ℝ) fun (n : ℕ) ↦
    ‖HMul.hMul (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
        ((↑(↑r : ℝ) : ℂ) ^ n)‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) *
      |(↑r : ℝ)| ^ n

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

Premises used: norm_pow, norm_mul, Complex.norm_real, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ ‖(↑(↑r : ℝ) : ℂ)‖ < 1

Tactic:
simpa using hr
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    ‖HMul.hMul (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
        ((↑(↑r : ℝ) : ℂ) ^ n)‖

Tactic:
exact (UpperHalfPlane.hasSum_qExpansion_of_norm_lt hh hfper hfhol hfbdd
    (by simpa using hr)).summable.norm

Premises used: HasSum.summable, Summable.norm, UpperHalfPlane.hasSum_qExpansion_of_norm_lt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
⊢ 0 < (Periodic.invQParam h q).im

Tactic:
have h1 := Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq1
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
⊢ Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)

Tactic:
have h2 := (Periodic.cuspFunction_eq_of_nonzero h (f ∘ ofComplex) hq1)
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)
⊢ cuspFunction h f q = f τ

Tactic:
simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1] using h2

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)
⊢ cuspFunction h f q = f τ

Tactic:
have : cuspFunction h f q = f τ := by simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1] using h2
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)
this : cuspFunction h f q = f τ
⊢ HasSum (fun (m : ℕ) ↦ c m • q ^ m) (cuspFunction h f q)

Tactic:
grind [hf τ, Periodic.qParam_right_inv]

Premises used: Function.Periodic.qParam_right_inv
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r_le : 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
r_pos : LT.lt (α := ENNReal) 0 1
hasSum :
  ∀ {y : ℂ},
    Membership.mem (γ := Set ℂ) (eball 0 1) y →
      HasSum (fun (n : ℕ) ↦ (FormalMultilinearSeries.ofScalars ℂ c n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ y)
        (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) (0 + y))
⊢ HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r_le : ∀ (r : ENNReal) (hr : r < 1), r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
⊢ 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r : ENNReal
hr : r < 1
r_le : ∀ (hr : LT.lt (α := ENNReal) 0 1), 0 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
r_le₁ : ∀ (hr' : r ≠ 0), r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
⊢ r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
rcases eq_or_ne r 0 with rfl | hr'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
hr : LT.lt (α := ENNReal) 0 1
⊢ 0 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r : ENNReal
hr : r < 1
hr' : r ≠ 0
⊢ r ≠ ⊤

Tactic:
hr.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r : ENNReal
hr : r < 1
hr' : r ≠ 0
r_le :
  ∀ (r : NNReal) (hr : (↑r : ENNReal) < 1) (hr' : (↑r : ENNReal) ≠ 0),
    (↑r : ENNReal) ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
⊢ r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
lift r to NNReal using hr.ne_top

Premises used: LT.lt.ne_top, NNReal