awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
| (2 * (↑π : ℂ) * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have enter : 0
Tactic: enter [1, 2, 2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
| 0
have rw : 0 * (2 * π / h)
Tactic: rw [show 0 = 0 * (2 * π / h) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
| (2 * (↑π : ℂ) * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have enter : 0 * (2 * π / h)
Tactic: enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
⊢ (2 * (↑π : ℂ) * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have conv : (2 * (↑π : ℂ) * Complex.I)⁻¹ *
    ∫ (θ : ℝ) in 0 * (2 * π / h)..h * (2 * π / h),
      deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
  1 / (↑h : ℂ) *
    ∫ (u : ℝ) in 0..h,
      1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := sorry : ℍ }
Tactic: conv => enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
⊢ (2 * (↑π : ℂ) * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0 * (2 * π / h)..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have simp_rw : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..h,
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
      deriv (circleMap 0 R) (x * (2 * π / h)) •
        (cuspFunction h f (circleMap 0 R (x * (2 * π / h))) / circleMap 0 R (x * (2 * π / h)) ^ (n + 1)))
  (∫ (x : ℝ) in 0..h,
    1 / (↑h : ℂ) *
      (1 / 𝕢 h ((↑x : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑x : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := sorry : ℍ }))
Tactic: simp_rw [← intervalIntegral.smul_integral_comp_mul_right, real_smul, ← mul_assoc,
    ← intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..h,
      (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
        deriv (circleMap 0 R) (x * (2 * π / h)) •
          (cuspFunction h f (circleMap 0 R (x * (2 * π / h))) / circleMap 0 R (x * (2 * π / h)) ^ (n + 1)))
    (∫ (x : ℝ) in 0..h,
      1 / (↑h : ℂ) *
        (1 / 𝕢 h ((↑x : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n *
          f { coe := (↑x : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }))
have e_f : ∀ (u : ℝ),
  (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 := sorry : ℍ })
Tactic: congr 1 with u
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 (↑τ : ℂ)
have simp : cexp ((↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I) = 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ))
Tactic: simp only [circleMap, ofReal_exp, ← exp_add, zero_add, τ, R]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 := ⋯ }
⊢ cexp ((↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I) = 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ))
have e_z : (↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I =
  2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) / (↑h : ℂ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 := ⋯ }
⊢ (↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) / (↑h : ℂ)
have e_z : -2 * (↑π : ℂ) * (↑t : ℂ) / (↑h : ℂ) + (↑u : ℂ) * (2 * (↑π : ℂ) / (↑h : ℂ)) * Complex.I =
  2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * Complex.I) / (↑h : ℂ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
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 := ⋯ }
⊢ -2 * (↑π : ℂ) * (↑t : ℂ) / (↑h : ℂ) + (↑u : ℂ) * (2 * (↑π : ℂ) / (↑h : ℂ)) * Complex.I =
    2 * (↑π : ℂ) * Complex.I * ((↑u : ℂ) + (↑t : ℂ) * Complex.I) / (↑h : ℂ)
have this : HPow.hPow (β := ℕ) Complex.I 2 = -1
Tactic: have := I_sq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
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 := ⋯ }
⊢ (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 := ⋯ : ℍ })
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 * (↑π : ℂ) * 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 := ⋯ : ℍ })
have e_f : (2 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
    (𝕢 h (↑τ : ℂ) * Complex.I * (f τ / (𝕢 h (↑τ : ℂ) ^ n * 𝕢 h (↑τ : ℂ)))) =
  1 / (↑h : ℂ) * (1 / 𝕢 h (↑τ : ℂ) ^ n * f τ)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 * (↑π : ℂ) * Complex.I)⁻¹ * (↑(2 * π / h) : ℂ) *
      (𝕢 h (↑τ : ℂ) * Complex.I * (f τ / (𝕢 h (↑τ : ℂ) ^ n * 𝕢 h (↑τ : ℂ)))) =
    1 / (↑h : ℂ) * (1 / 𝕢 h (↑τ : ℂ) ^ n * f τ)
have e_f : (↑(2 * π / h) : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)
Tactic: field_simp [(show 𝕢 h τ ≠ 0 from Complex.exp_ne_zero _), Real.pi_ne_zero, NeZero.ne]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 : ℂ)
have e_f : 2 * (↑π : ℂ) / (↑h : ℂ) * f τ = 2 * (↑π : ℂ) * f τ / (↑h : ℂ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f τ - valueAtInfty f) fun (τ : ℍ) ↦
    rexp (-2 * π * τ.im / h)
have this : Asymptotics.IsBigO (F := ℝ) I∞ (f ∘ (↑ofComplex : ℂ → ℍ)) (1 ∘ (↑ofComplex : ℂ → ℍ))
Tactic: have := hfbdd.comp_tendsto tendsto_comap_im_ofComplex
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 : ℂ → ℍ))
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f τ - valueAtInfty f) fun (τ : ℍ) ↦
    rexp (-2 * π * τ.im / h)
have h₁ : ∀ (x : ℍ),
  f x - valueAtInfty f =
    ((fun (z : ℂ) ↦ (f ∘ (↑ofComplex : ℂ → ℍ)) z - Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) 0) ∘
        UpperHalfPlane.coe)
      x
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
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 Γ)
⊢ ∃ c > 0,
    Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
      (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
      rexp (-c * τ.im)
have hh : 0 < Γ.strictWidthInfty
Tactic: have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
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
⊢ ∃ c > 0,
    Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
      (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
      rexp (-c * τ.im)
have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
Tactic: have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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)
have refine : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
  (fun (τ : ℍ) ↦ HSub.hSub (α := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) (valueAtInfty (⇑f : (a : ℍ) → ℂ))) fun (τ : ℍ) ↦
  rexp (-(2 * π / Γ.strictWidthInfty) * τ.im)
Tactic: refine ⟨2 * π / Γ.strictWidthInfty, div_pos Real.two_pi_pos hh, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 * π / Γ.strictWidthInfty) * τ.im)
have h : ∀ (τ : ℍ), -(2 * π / Γ.strictWidthInfty) * τ.im = -2 * π * τ.im / Γ.strictWidthInfty
Tactic: convert! exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) using
    3 with τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ Periodic.cuspFunction h (f * g) 0 = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0
have rw : limUnder (𝓝[≠] 0) ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0
Tactic: rw [Periodic.cuspFunction, update_self]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f * g) = cuspFunction h f * cuspFunction h g
have h₁ : ∀ (z : ℂ), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
have pos : ∀ (H : z = 0), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
Tactic: by_cases H : z = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
have neg : ∀ (H : ¬z = 0), cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
Tactic: by_cases H : z = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ qExpansion h (f * g) = qExpansion h f * qExpansion h g
have h₁ : ∀ (n : ℕ),
  Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f * g)) : ℂ)
    ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f * qExpansion h g) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n : ℕ
⊢ Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f * g)) : ℂ)
    ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f * qExpansion h g) : ℂ)
have h₁ : Eq (α := ℂ)
  (∑ i ∈ Finset.range (n + 1),
    (↑n.factorial : ℂ)⁻¹ *
      ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0))
  (∑ x ∈ Finset.range (n + 1),
    (↑x.factorial : ℂ)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
      ((↑(n - x).factorial : ℂ)⁻¹ * iteratedDeriv (n - x) (cuspFunction h g) 0))
Tactic: simp only [qExpansion_coeff, cuspFunction_mul hf.continuousAt hg.continuousAt,
    iteratedDeriv_mul hf.contDiffAt hg.contDiffAt, Finset.mul_sum, PowerSeries.coeff_mul,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n : ℕ
⊢ Eq (α := ℂ)
    (∑ i ∈ Finset.range (n + 1),
      (↑n.factorial : ℂ)⁻¹ *
        ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0))
    (∑ x ∈ Finset.range (n + 1),
      (↑x.factorial : ℂ)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
        ((↑(n - x).factorial : ℂ)⁻¹ * iteratedDeriv (n - x) (cuspFunction h g) 0))
have h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
  (↑n.factorial : ℂ)⁻¹ *
      ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0) =
    (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)
Tactic: refine Finset.sum_congr rfl fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (↑n.factorial : ℂ)⁻¹ *
      ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0) =
    (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)
have h₁ : (↑n.factorial : ℂ)⁻¹ *
    ((↑n.factorial : ℂ) / HMul.hMul (α := ℂ) (↑i.factorial : ℂ) (↑(n - i).factorial : ℂ) *
        iteratedDeriv i (cuspFunction h f) 0 *
      iteratedDeriv (n - i) (cuspFunction h g) 0) =
  (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
    ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)
Tactic: rw [Nat.cast_choose _ (by grind)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
a : ℂ
⊢ qExpansion h (a • f) = a • qExpansion h f
have h₁ : ∀ (m : ℕ),
  Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (a • f)) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (a • qExpansion h f) : ℂ)
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ qExpansion h (f + g) = qExpansion h f + qExpansion h g
have h₁ : ∀ (m : ℕ),
  Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f + g)) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f + qExpansion h g) : ℂ)
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ qExpansion h (f - g) = qExpansion h f - qExpansion h g
have hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0
Tactic: have hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0 := by
    simpa [cuspFunction_neg hg.continuousAt] using hg.neg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
this : cuspFunction h 0 = 0
⊢ qExpansion h 0 = 0
have h₁ : ∀ (n : ℕ),
  Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h 0) : ℂ)
    ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) 0 : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
⊢ qExpansion h 0 = 0
have suffices : cuspFunction h 0 = 0
Tactic: suffices cuspFunction h 0 = 0 by ext; simp [qExpansion_coeff, this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ qExpansion h f = 0 ↔ f = 0
have mp : qExpansion h f = 0 → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
mp : qExpansion h f = 0 → f = 0
⊢ qExpansion h f = 0 ↔ f = 0
have mpr : f = 0 → qExpansion h f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : qExpansion h f = 0
⊢ f = 0
have mp : ∀ (z : ℍ), f z = 0 z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
⊢ qExpansion h 1 = 1
have h₁ : ∀ (m : ℕ),
  Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h 1) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) 1 : ℂ)
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
m : ℕ
⊢ cuspFunction h 1 = 1
have h₁ : ∀ (q : ℂ), cuspFunction h 1 q = 1 q
Tactic: ext q
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
m : ℕ
q : ℂ
⊢ cuspFunction h 1 q = 1 q
have h₁ : cuspFunction h 1 0 = 1 0
Tactic: rcases eq_or_ne q 0 with rfl | hq
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
m : ℕ
q : ℂ
h₁ : cuspFunction h 1 0 = 1 0
⊢ cuspFunction h 1 q = 1 q
have h₂ : ∀ (hq : q ≠ 0), cuspFunction h 1 q = 1 q
Tactic: rcases eq_or_ne q 0 with rfl | hq