awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
have r_le : ∀ (r : ENNReal) (hr : r < 1), r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
Tactic: refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r : ENNReal
hr : r < 1
⊢ r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
have r_le : ∀ (hr : LT.lt (α := ENNReal) 0 1), 0 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
Tactic: rcases eq_or_ne r 0 with rfl | hr'
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
have r_le₁ : ∀ (hr' : r ≠ 0), r ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
Tactic: rcases eq_or_ne r 0 with rfl | hr'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
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 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
have r_le : ∀ (r : NNReal) (hr : (↑r : ENNReal) < 1) (hr' : (↑r : ENNReal) ≠ 0),
  (↑r : ENNReal) ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
Tactic: lift r to NNReal using hr.ne_top
Cleared hypotheses: r, hr, hr'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r : NNReal
hr : (↑r : ENNReal) < 1
hr' : (↑r : ENNReal) ≠ 0
this : FiniteDimensional ℝ ℂ := ⋯
⊢ (↑r : ENNReal) ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
have r_le : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) ℂ) (FormalMultilinearSeries.ofScalars ℂ c n) *
    (↑r : ℝ) ^ n
Tactic: apply FormalMultilinearSeries.le_radius_of_summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
y : ℂ
hy : 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))
have hasSum : 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) y)
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
y : ℂ
hy : 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) y)
have hy₁ : ‖y‖ < 1
Tactic: rw [← ENNReal.coe_one, Metric.eball_coe, NNReal.coe_one, mem_ball_zero_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
⊢ 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) y)
have hasSum : ∀ (hy : norm (E := ℂ) 0 < 1),
  HasSum (fun (n : ℕ) ↦ (FormalMultilinearSeries.ofScalars ℂ c n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 0)
    (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) 0)
Tactic: rcases eq_or_ne y 0 with rfl | hy'
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
hasSum :
  ∀ (hy : norm (E := ℂ) 0 < 1),
    HasSum (fun (n : ℕ) ↦ (FormalMultilinearSeries.ofScalars ℂ c n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ 0)
      (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) 0)
⊢ 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) y)
have hasSum₁ : ∀ (hy' : y ≠ 0),
  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) y)
Tactic: rcases eq_or_ne y 0 with rfl | hy'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have H1 : HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c)
  0 1
Tactic: have H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (.ofScalars ℂ c) 0 1 :=
    hasFPowerSeriesOnBall_update hh hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
⊢ c 0 = cuspFunction h f 0
have L1 : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0
Tactic: have L1 := H1.hasFPowerSeriesAt.continuousAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0
⊢ c 0 = cuspFunction h f 0
have L2 : ContinuousAt (cuspFunction h f) 0
Tactic: have L2 := hfanalytic.continuousAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) =ᶠ[𝓝[≠] 0] cuspFunction h f
have h₁ : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {0}ᶜ x →
        Membership.mem (γ := Set ℂ)
          {x : ℂ | (fun (x : ℂ) ↦ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) x = cuspFunction h f x) x} x}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
h₁ :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {0}ᶜ x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ | (fun (x : ℂ) ↦ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) x = cuspFunction h f x) x}
            x}
      a
⊢ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) =ᶠ[𝓝[≠] 0] cuspFunction h f
have h₂ : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ) {0}ᶜ a → update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) a = cuspFunction h f a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
⊢ c 0 = cuspFunction h f 0
have this : update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
Tactic: have := (L1.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE L2).mp <|
      by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have H2 : c 0 = cuspFunction h f 0
Tactic: have H2 : c 0 = cuspFunction h f 0 := by
    have L1 := H1.hasFPowerSeriesAt.continuousAt
    have L2 := hfanalytic.continuousAt
    have := (L1.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE L2).mp <|
      by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
    simpa [update_self] using this.eq_of_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
H1 :
  HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
H2 : c 0 = cuspFunction h f 0
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have rwa : ∀ (H1 : HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1)
  (H2 : c 0 = cuspFunction h f 0), HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
Tactic: rwa [update_eq_self_iff.mpr H2] at H1
Cleared hypotheses: H1, H2
-- 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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have this : ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
  (2 * (↑π : ℂ) * Complex.I / (↑n.factorial : ℂ)) • iteratedDeriv n (cuspFunction h f) 0
Tactic: have := ((differentiableOn_cuspFunction_ball hh hfper hfhol hfbdd).mono
    (Metric.closedBall_subset_ball hR')).circleIntegral_one_div_sub_center_pow_smul hR n
-- 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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    (2 * (↑π : ℂ) * Complex.I / (↑n.factorial : ℂ)) • iteratedDeriv n (cuspFunction h f) 0
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have this₁ : (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
  (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
Tactic: rw [smul_eq_mul, div_eq_mul_inv, mul_assoc, mul_comm, ← div_eq_iff two_pi_I_ne_zero] at this
Cleared hypotheses: 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
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw : (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
    (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
simp_rw :
  (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
      (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw₁ : (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
simp_rw :
  (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
      (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₁ :
  (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw₂ : (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
simp_rw :
  (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
      (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₁ :
  (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₂ :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw₃ : (∮ (z : ℂ) in C(0, R), (1 / z ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
simp_rw :
  (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
      (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₁ :
  (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₂ :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₃ :
  (∮ (z : ℂ) in C(0, R), (1 / z ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw₄ : (∮ (z : ℂ) in C(0, R), 1 / z ^ (n + 1) * cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
simp_rw :
  (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ)
      (PowerSeries.mk fun (m : ℕ) ↦ (↑m.factorial : ℂ)⁻¹ * iteratedDeriv m (cuspFunction h f) 0) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₁ :
  (↑n.factorial : ℂ)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₂ :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₃ :
  (∮ (z : ℂ) in C(0, R), (1 / z ^ (n + 1)) • cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
simp_rw₄ :
  (∮ (z : ℂ) in C(0, R), 1 / z ^ (n + 1) * cuspFunction h f z) / (2 * (↑π : ℂ) * Complex.I) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
have simp_rw₅ : (∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)) / (2 * (↑π : ℂ) * Complex.I) =
  (2 * (↑π : ℂ) * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Tactic: simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_mul]
-- 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)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have hR0 : 0 < R
Tactic: have hR0 : 0 < R := Real.exp_pos _
-- 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
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have hR1 : R < 1
Tactic: have hR1 : R < 1 := Real.exp_lt_one_iff.2 <| by simpa [neg_div] using div_pos (by positivity) hh
-- 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
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    1 / (↑h : ℂ) *
      ∫ (u : ℝ) in 0..h,
        1 / 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)) ^ n * f { coe := (↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ), coe_im_pos := ⋯ : ℍ }
have rw : (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 := sorry : ℍ }
Tactic: rw [qExpansion_coeff_eq_circleIntegral hh hfper hfhol hfbdd n hR0 hR1, circleIntegral,
    show 2 * π = h * (2 * π / h) by field_simp]