awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
e_z :
  (↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) / (↑h : ℂ)
⊢ cexp ((↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I) = 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
e_z :
  -2 * (↑π : ℂ) * (↑t : ℂ) / (↑h : ℂ) + (↑u : ℂ) * (2 * (↑π : ℂ) / (↑h : ℂ)) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * Complex.I) / (↑h : ℂ)
⊢ (↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) / (↑h : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
⊢ HPow.hPow (β := ℕ) Complex.I 2 = -1

Tactic:
have := I_sq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : HPow.hPow (β := ℕ) Complex.I 2 = -1
⊢ -2 * (↑π : ℂ) * (↑t : ℂ) / (↑h : ℂ) + (↑u : ℂ) * (2 * (↑π : ℂ) / (↑h : ℂ)) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * Complex.I) / (↑h : ℂ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
⊢ circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)

Tactic:
have : circleMap 0 R (u * (2 * π / h)) = 𝕢 h τ := by
    simp only [circleMap, ofReal_exp, ← exp_add, zero_add, τ, R]
    congr 1
    push_cast
    have := I_sq
    grind
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
⊢ (↑I : ℂ) = Complex.I

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
⊢ (↑u : ℂ) + (↑t : ℂ) * Complex.I = (↑τ : ℂ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
⊢ { coe := (↑τ : ℂ), coe_im_pos := ⋯ : ℍ } = τ

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
e_f :
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
      (𝕢 h (↑τ : ℂ) * Complex.I * (f τ / (𝕢 h (↑τ : ℂ) ^ n * 𝕢 h (↑τ : ℂ)))) =
    1 / (↑h : ℂ) * (1 / 𝕢 h (↑τ : ℂ) ^ n * f τ)
⊢ (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
      deriv (circleMap 0 R) (u * (2 * π / h)) •
        (cuspFunction h f (circleMap 0 R (u * (2 * π / h))) / circleMap 0 R (u * (2 * π / h)) ^ (n + 1)) =
    1 / (↑h : ℂ) *
      (1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ })

Tactic:
simp_rw [deriv_circleMap, this, show ↑I = Complex.I by rfl, show u + t * Complex.I = τ by rfl,
    show ⟨↑τ, τ.2⟩ = τ by rfl, eq_cuspFunction _ hh.ne' hfper, smul_eq_mul, pow_succ]

Premises used: pow_succ, UpperHalfPlane.eq_cuspFunction, LT.lt.ne', deriv_circleMap, 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
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
e_f : (↑(2 * π / h) : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)
⊢ (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
      (𝕢 h (↑τ : ℂ) * Complex.I * (f τ / (𝕢 h (↑τ : ℂ) ^ n * 𝕢 h (↑τ : ℂ)))) =
    1 / (↑h : ℂ) * (1 / 𝕢 h (↑τ : ℂ) ^ n * f τ)

Tactic:
field_simp [(show 𝕢 h τ ≠ 0 from Complex.exp_ne_zero _), Real.pi_ne_zero, NeZero.ne]

Premises used: Real.pi, HMul.hMul, Complex.exp_ne_zero, UpperHalfPlane.coe, HDiv.hDiv, Complex.ofReal, OfNat.ofNat, Real.pi_ne_zero, NeZero.ne, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
e_f : 2 * (↑π : ℂ) / (↑h : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)
⊢ (↑(2 * π / h) : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)
⊢ 2 * (↑π : ℂ) / (↑h : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ Asymptotics.IsBigO (F := ℝ) I∞ (f ∘ (↑ofComplex : ℂ → ℍ)) (1 ∘ (↑ofComplex : ℂ → ℍ))

Tactic:
have := hfbdd.comp_tendsto tendsto_comap_im_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : Asymptotics.IsBigO (F := ℝ) I∞ (f ∘ (↑ofComplex : ℂ → ℍ)) (1 ∘ (↑ofComplex : ℂ → ℍ))
z : ℂ
hz : z ∈ Complex.im ⁻¹' Ioi 0
⊢ DifferentiableAt ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) z

Tactic:
simpa using (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩)

Premises used: UpperHalfPlane.mk, Iff.mp, UpperHalfPlane.mdifferentiableAt_iff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : Asymptotics.IsBigO (F := ℝ) I∞ (f ∘ (↑ofComplex : ℂ → ℍ)) (1 ∘ (↑ofComplex : ℂ → ℍ))
h₁ :
  ∀ (x : ℍ),
    f x - valueAtInfty f =
      ((fun (z : ℂ) ↦ (f ∘ (↑ofComplex : ℂ → ℍ)) z - Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) 0) ∘
          UpperHalfPlane.coe)
        x
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f τ - valueAtInfty f) fun (τ : ℍ) ↦
    rexp (-2 * π * τ.im / h)

Tactic:
convert!
    (hfper.exp_decay_sub_of_bounded_at_inf hh
          (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0)) fun z hz ↦ by
            simpa using (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩))
          this).comp_tendsto
      tendsto_coe_atImInfty

Premises used: Filter.Ioi_mem_atTop, Filter.eventually_of_mem, Filter.preimage_mem_comap, Asymptotics.IsBigO.comp_tendsto, UpperHalfPlane.tendsto_coe_atImInfty, OfNat.ofNat, Function.Periodic.exp_decay_sub_of_bounded_at_inf
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : Asymptotics.IsBigO (F := ℝ) I∞ (f ∘ (↑ofComplex : ℂ → ℍ)) (1 ∘ (↑ofComplex : ℂ → ℍ))
x : ℍ
⊢ f x - valueAtInfty f =
    ((fun (z : ℂ) ↦ (f ∘ (↑ofComplex : ℂ → ℍ)) z - Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) 0) ∘
        UpperHalfPlane.coe)
      x

Tactic:
simpa [cuspFunction] using
    (cuspFunction_apply_zero hh (analyticAt_cuspFunction_zero hh hfper hfhol hfbdd) hfper).symm

Premises used: UpperHalfPlane.cuspFunction, UpperHalfPlane.analyticAt_cuspFunction_zero, Eq.symm, UpperHalfPlane.cuspFunction_apply_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
f : ℍ → ℂ
hf : IsZeroAtImInfty f
⊢ I∞.ZeroAtFilter (f ∘ (↑ofComplex : ℂ → ℍ))

Tactic:
hf.comp tendsto_comap_im_ofComplex

Premises used: Filter.ZeroAtFilter, Filter.Tendsto.comp, UpperHalfPlane.tendsto_comap_im_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hf : IsZeroAtImInfty f
hh : 0 < h
⊢ cuspFunction h f 0 = 0

Tactic:
Periodic.cuspFunction_zero_of_zero_at_inf hh hf.zero_at_infty_comp_ofComplex

Premises used: UpperHalfPlane.cuspFunction, Function.Periodic.cuspFunction_zero_of_zero_at_inf, UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hf : IsZeroAtImInfty f
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ Asymptotics.IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ rexp (-2 * π * τ.im / h)

Tactic:
simpa [hf.valueAtInfty_eq_zero] using exp_decay_sub_atImInfty hh hfper hfhol hfbdd

Premises used: UpperHalfPlane.exp_decay_sub_atImInfty, UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero
-- 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
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < ((↑u : ℂ) + (↑t : ℂ) * I).im

Tactic:
simpa using ht
-- 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
n : ℕ
t : ℝ
ht : 0 < t
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        HMul.hMul (β := ℂ) (1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * I) ^ n)
          ((f : (a : ℍ) → ℂ) { coe := (↑u : ℂ) + (↑t : ℂ) * I, coe_im_pos := ⋯ : ℍ } : ℂ)

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

Premises used: SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, Fact.mk, Subgroup.isCusp_of_mem_strictPeriods, ModularFormClass.holo, UpperHalfPlane.qExpansion_coeff_eq_intervalIntegral, Complex.I
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
⊢ 0 < Γ.strictWidthInfty

Tactic:
have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
⊢ Γ.strictWidthInfty ∈ Γ.strictPeriods

Tactic:
have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
⊢ ∃ c > 0,
    Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
      (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
      rexp (-c * τ.im)

Tactic:
⟨2 * π / Γ.strictWidthInfty, div_pos Real.two_pi_pos hh, ?_⟩

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Real.two_pi_pos, And.intro, Exists.intro, div_pos, OfNat.ofNat, Subgroup.strictWidthInfty
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
refine :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
    rexp (-(2 * π / Γ.strictWidthInfty) * τ.im)
⊢ ∃ c > 0,
    Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
      (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
      rexp (-c * τ.im)

Tactic:
refine ⟨2 * π / Γ.strictWidthInfty, div_pos Real.two_pi_pos hh, ?_⟩
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
    rexp (-2 * π * τ.im / Γ.strictWidthInfty)

Tactic:
exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f)

Premises used: UpperHalfPlane.exp_decay_sub_atImInfty, SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, ModularFormClass.holo
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
h : ∀ (τ : ℍ), -(2 * π / Γ.strictWidthInfty) * τ.im = -2 * π * τ.im / Γ.strictWidthInfty
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
    rexp (-(2 * π / Γ.strictWidthInfty) * τ.im)

Tactic:
convert! exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) using
    3 with τ

Premises used: UpperHalfPlane.exp_decay_sub_atImInfty, SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, ModularFormClass.holo
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
τ : ℍ
⊢ -(2 * π / Γ.strictWidthInfty) * τ.im = -2 * π * τ.im / Γ.strictWidthInfty

Tactic:
ring_nf
-- 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
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
hf : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ ∃ c > 0, Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ rexp (-c * τ.im)

Tactic:
simpa [hf.valueAtInfty_eq_zero] using exp_decay_sub_atImInfty' f

Premises used: UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero, ModularFormClass.exp_decay_sub_atImInfty'
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst_1 : CuspFormClass F Γ k
inst_2 : Fact (IsCusp OnePoint.infty Γ)
⊢ I∞.ZeroAtFilter (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))

Tactic:
(zero_at_infty f).comp tendsto_comap_im_ofComplex

Premises used: CuspFormClass.zero_at_infty, Filter.ZeroAtFilter, Filter.Tendsto.comp, 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 : CuspFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
⊢ cuspFunction h (⇑f : (a : ℍ) → ℂ) 0 = 0

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
  (CuspFormClass.zero_at_infty f).cuspFunction_apply_zero hh

Premises used: CuspFormClass.zero_at_infty, Fact.mk, Subgroup.isCusp_of_mem_strictPeriods, UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : CuspFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)

Tactic:
simp [qExpansion_coeff, cuspFunction_apply_zero f hh hΓ]

Premises used: UpperHalfPlane.qExpansion_coeff, CuspFormClass.cuspFunction_apply_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : CuspFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ rexp (-2 * π * τ.im / h)

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
  UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty (CuspFormClass.zero_at_infty f) hh
    (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f)

Premises used: CuspFormClass.holo, CuspFormClass.zero_at_infty, SlashInvariantFormClass.periodic_comp_ofComplex, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty, ModularFormClass.bdd_at_infty, Fact.mk, Subgroup.isCusp_of_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst_1 : CuspFormClass F Γ k
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : DiscreteTopology ↥Γ
inst_4 : Fact (IsCusp OnePoint.infty Γ)
⊢ ∃ c > 0, Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ rexp (-c * τ.im)

Tactic:
ModularFormClass.exp_decay_atImInfty' f (CuspFormClass.zero_at_infty f)

Premises used: CuspFormClass.zero_at_infty, ModularFormClass.exp_decay_atImInfty'
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
rw : limUnder (𝓝[≠] 0) ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0
⊢ Periodic.cuspFunction h (f * g) 0 = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
rw [Periodic.cuspFunction, update_self]

Premises used: Function.Periodic.cuspFunction, Function.update_self
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ limUnder (𝓝[≠] 0) ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
(Periodic.tendsto_nhds_zero hfcts).mul (Periodic.tendsto_nhds_zero hgcts) |>.limUnder_eq

Premises used: Function.Periodic.tendsto_nhds_zero, Filter.Tendsto.mul, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ limUnder (𝓝[≠] 0) ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
exact (Periodic.tendsto_nhds_zero hfcts).mul (Periodic.tendsto_nhds_zero hgcts) |>.limUnder_eq

Premises used: Function.Periodic.tendsto_nhds_zero, Filter.Tendsto.mul, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ (PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f * g)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ)
      ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion h g) : ℂ)

Tactic:
simpa [qExpansion_coeff] using cuspFunction_mul_zero hfcts hgcts

Premises used: UpperHalfPlane.qExpansion_coeff, UpperHalfPlane.cuspFunction_mul_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
h₁ : ∀ (z : ℂ), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
⊢ cuspFunction h (f * g) = cuspFunction h f * cuspFunction h g

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
pos : ∀ (H : z = 0), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
neg : ∀ (H : ¬z = 0), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z

Tactic:
by_cases H : z = 0
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
H : z = 0
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z

Tactic:
simpa [H] using cuspFunction_mul_zero hfcts hgcts

Premises used: UpperHalfPlane.cuspFunction_mul_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
H : ¬z = 0
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z

Tactic:
simp [cuspFunction, Periodic.cuspFunction, H]

Premises used: Function.Periodic.cuspFunction, UpperHalfPlane.cuspFunction
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
a : ℂ
⊢ cuspFunction h (a • f) = a • cuspFunction h f

Tactic:
apply Periodic.cuspFunction_smul hfcts

Premises used: Function.Periodic.cuspFunction_smul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
⊢ cuspFunction h (-f) = -cuspFunction h f

Tactic:
Periodic.cuspFunction_neg hfcts

Premises used: Function.Periodic.cuspFunction_neg, UpperHalfPlane.cuspFunction