awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ Eq (α := ℍ → ℂ) (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ)
    (((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) ∘ UpperHalfPlane.coe)

Tactic:
exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm

Premises used: UpperHalfPlane.comp_ofComplex, funext, EisensteinSeries.eisensteinSeriesSIF, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
suffices : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) τ

Tactic:
suffices DifferentiableAt ℂ (↑ₕeisensteinSeriesSIF a k) τ.1 by
    convert!
      MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
    exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds, UpperHalfPlane.coe_im_pos, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
refine :
  DifferentiableOn ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) upperHalfPlaneSet
⊢ DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds, UpperHalfPlane.coe_im_pos, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableOn ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) upperHalfPlaneSet

Tactic:
(eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
    (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
    fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet

Premises used: Filter.Eventually.of_forall, DifferentiableOn.fun_sum, TendstoLocallyUniformlyOn.differentiableOn, EisensteinSeries.eisSummand_extension_differentiableOn, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, Subtype.val, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableOn ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) upperHalfPlaneSet

Tactic:
exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
    (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
    fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet

Premises used: Filter.Eventually.of_forall, DifferentiableOn.fun_sum, TendstoLocallyUniformlyOn.differentiableOn, EisensteinSeries.eisSummand_extension_differentiableOn, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, Subtype.val, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
apply :
  EqOn (β := ℂ) (iteratedDeriv k fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ)))
    (fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S
⊢ EqOn (β := ℂ) (iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S)
    (fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S

Tactic:
apply EqOn.trans (iteratedDerivWithin_of_isOpen hs)

Premises used: Set.EqOn.trans, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
h : ∀ (z : ℂ), cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * z / (↑p : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * z)
⊢ Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
z : ℂ
⊢ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * z / (↑p : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * z)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)

Tactic:
have : (fun s ↦ cexp (2 * π * I * m * s / p)) = fun s ↦ cexp (((2 * π * I * m) / p) * s) := by
    ext z
    ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this :
  Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)
simp :
  (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * x) =
    (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * x / (↑p : ℂ))
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)
    ((fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)

Tactic:
simp only [this, iteratedDeriv_cexp_const_mul]

Premises used: iteratedDeriv_cexp_const_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this :
  Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)
⊢ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * x) =
    (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * x / (↑p : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h :
  ∀ (z : ℕ),
    (2 * (↑π : ℂ) * I * (↑z : ℂ) / (↑p : ℂ)) ^ k = (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑z : ℂ) k
⊢ Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
z : ℕ
⊢ (2 * (↑π : ℂ) * I * (↑z : ℂ) / (↑p : ℂ)) ^ k = (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑z : ℂ) k

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k

Tactic:
have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
      ext z
      ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h1 :
  Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
simpa [h1] using isBigO_ofReal_right.mp (Asymptotics.isBigO_const_mul_self
      ((2 * π * I / p) ^ k) (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)) atTop)

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, Nat.cast, Filter.atTop, HPow.hPow, Iff.mp, Asymptotics.isBigO_const_mul_self, Complex.isBigO_ofReal_right, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
have h0 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =O[atTop] fun n ↦ ((n ^ k) : ℝ) := by
    have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
      ext z
      ring
    simpa [h1] using isBigO_ofReal_right.mp (Asymptotics.isBigO_const_mul_self
      ((2 * π * I / p) ^ k) (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)) atTop)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
push_cast :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (l + k)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ (↑(n ^ (l + k)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ f x * (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ)) ^ k)
    fun (x : ℕ) ↦ HPow.hPow (α := ℝ) (↑x : ℝ) l * HPow.hPow (α := ℝ) (↑x : ℝ) k

Tactic:
hf.mul h0

Premises used: Asymptotics.IsBigO.mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
h : ∀ (x : ℕ), HPow.hPow (α := ℝ) (↑x : ℝ) (l + k) = HPow.hPow (α := ℝ) (↑x : ℝ) l * HPow.hPow (α := ℝ) (↑x : ℝ) k
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (l + k)

Tactic:
convert! hf.mul h0

Premises used: Asymptotics.IsBigO.mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
x : ℕ
⊢ HPow.hPow (α := ℝ) (↑x : ℝ) (l + k) = HPow.hPow (α := ℝ) (↑x : ℝ) l * HPow.hPow (α := ℝ) (↑x : ℝ) k

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
apply :
  ∀ K ⊆ ℍₒ,
    IsCompact K →
      ∃ (u : ℕ → ℝ),
        Summable u ∧
          ∀ (n : ℕ),
            ∀ k_1 ∈ K,
              ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                    (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
                u n
⊢ SummableLocallyUniformlyOn (α := ℂ)
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ))
    ℍₒ

Tactic:
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet

Premises used: SummableLocallyUniformlyOn_of_locally_bounded, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ CompactSpace (↑K : Type)

Tactic:
have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
⊢ Continuous (Y := ℂ) fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
simp : ∀ (x : (↑K : Type)), ‖cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))‖ < 1
⊢ ‖r‖ < 1

Tactic:
simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]

Premises used: BoundedContinuousFunction.mkOfCompact_apply, norm_norm, Real.zero_lt_one, BoundedContinuousFunction.norm_lt_iff_of_compact, ContinuousMap.coe_mk
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : (↑K : Type)
⊢ cexp (2 * (↑π : ℂ) * I * ((↑x : ℂ) / (↑p : ℂ))) = cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : (↑K : Type)
⊢ cexp (2 * (↑π : ℂ) * I * ((↑x : ℂ) / (↑p : ℂ))) = cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))

Tactic:
have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : (↑K : Type)
h1 : cexp (2 * (↑π : ℂ) * I * ((↑x : ℂ) / (↑p : ℂ))) = cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))
⊢ 0 < ((↑x : ℂ) / (↑p : ℂ)).im

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : (↑K : Type)
h1 : cexp (2 * (↑π : ℂ) * I * ((↑x : ℂ) / (↑p : ℂ))) = cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))‖ < 1

Tactic:
simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
⊢ ‖r‖ < 1

Tactic:
have hr : ‖r‖ < 1 := by
    simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]
    intro x
    have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
    simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n

Tactic:
simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf)))

Premises used: Iff.mpr, summable_norm_mul_geometric_of_norm_lt_one', Asymptotics.isBigO_norm_left, _private.0.aux_IsBigO_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
refine :
  ∀ (n : ℕ) (z : ℂ) (hz : z ∈ K),
    ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
          (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) z‖ ≤
      ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ K,
          ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
            u n

Tactic:
refine ⟨_, by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))), fun n z hz ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
⊢ norm (E := ℂ) ((mkOfCompact c : (a : (↑K : Type)) → ℂ) (Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z hz) : ℂ) ^ n ≤
    ‖mkOfCompact c‖ ^ n

Tactic:
have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  norm (E := ℂ) ((mkOfCompact c : (a : (↑K : Type)) → ℂ) (Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z hz) : ℂ) ^ n ≤
    ‖mkOfCompact c‖ ^ n
simp :
  ∀
    (hr :
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
            C((↑K : Type), ℂ) } <
        1),
    ‖f n‖ * ((2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖) ≤
      ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
        norm (E := C((↑K : Type), ℂ))
            { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
              C((↑K : Type), ℂ) } ^
          n
⊢ ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n

Tactic:
simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
    norm_natCast, abs_norm, ge_iff_le, r, c] at *

Premises used: norm_pow, ge_iff_le, Complex.norm_natCast, Complex.exp_nsmul', BoundedContinuousFunction.mkOfCompact_apply, norm_mul, Complex.norm_real, Complex.norm_div, Complex.norm_ofNat, _private.0.iteratedDerivWithin_cexp_aux, ContinuousMap.coe_mk, BoundedContinuousFunction.norm_mkOfCompact, Complex.norm_I, smul_eq_mul, abs_norm, mul_one, UpperHalfPlane.isOpen_upperHalfPlaneSet, Real.norm_eq_abs, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
rw :
  ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
            C((↑K : Type), ℂ) } ^
        n
⊢ ‖f n‖ * ((2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖) ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
            C((↑K : Type), ℂ) } ^
        n

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc