awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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_le :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) ℂ) (FormalMultilinearSeries.ofScalars ℂ c n) *
      (↑r : ℝ) ^ n
⊢ (↑r : ENNReal) ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)

Tactic:
apply FormalMultilinearSeries.le_radius_of_summable

Premises used: FormalMultilinearSeries.le_radius_of_summable
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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 : ℝ) : ℂ)‖ < 1

Tactic:
simpa using hr
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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 ℝ ℂ := ⋯
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap ℂ (fun (i : Fin n) ↦ ℂ) ℂ) (FormalMultilinearSeries.ofScalars ℂ c n) *
      (↑r : ℝ) ^ n

Tactic:
simpa [smul_eq_mul, norm_mul, mul_comm, mul_left_comm, mul_assoc] using
        (hasSum_cuspFunction_of_hasSum_punctured hh hf (q := r) (by simpa using hr)
          (mod_cast hr')).summable.norm

Premises used: ENNReal.ofNNReal, congrArg, mul_assoc, cast, Ne, norm_mul, _private.0.UpperHalfPlane.hasSum_cuspFunction_of_hasSum_punctured, mul_left_comm, Complex.ofReal, HasSum.summable, mul_comm, Summable.norm, ENNReal.coe_inj._simp_1, Nat.cast_zero, smul_eq_mul, NNReal.coe_inj._simp_1, Eq.symm, Eq, NNReal.toReal, Not, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ LT.lt (α := ENNReal) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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 :
  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)
⊢ 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))

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ ‖y‖ < 1

Tactic:
rw [← ENNReal.coe_one, Metric.eball_coe, NNReal.coe_one, mem_ball_zero_iff] at hy

Premises used: ENNReal.coe_one, NNReal.coe_one, Metric.eball_coe, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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₁ :
  ∀ (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)
⊢ 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'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
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:
simpa +contextual [zero_pow_eq] using hasSum_ite_eq 0 (c 0)

Premises used: hasSum_ite_eq, zero_pow_eq, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
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:
simpa [update_of_ne hy', mul_comm]
        using hasSum_cuspFunction_of_hasSum_punctured hh hf hy hy'

Premises used: _private.0.UpperHalfPlane.hasSum_cuspFunction_of_hasSum_punctured, mul_comm, Function.update_of_ne
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0)) 0

Tactic:
have L1 := H1.hasFPowerSeriesAt.continuousAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ ContinuousAt (cuspFunction h f) 0

Tactic:
have L2 := hfanalytic.continuousAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
a : ℂ
ha : Membership.mem (γ := Set ℂ) {0}ᶜ a
⊢ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) a = cuspFunction h f a

Tactic:
update_of_ne ha ..

Premises used: Function.update_of_ne
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
h₂ h₃ :
  ∀ (a : ℂ) (ha : Membership.mem (γ := Set ℂ) {0}ᶜ a),
    update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) a = cuspFunction h f a
⊢ update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) =ᶠ[𝓝[≠] 0] cuspFunction h f

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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

Tactic:
have := (L1.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE L2).mp <|
      by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
this : update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
⊢ c 0 = cuspFunction h f 0

Tactic:
simpa [update_self] using this.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, Function.update_self
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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

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
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
rwa rwa₁ rwa₂ 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
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
rwa [update_eq_self_iff.mpr H2] at H1

Premises used: Iff.mpr, Function.update_eq_self_iff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ ∮ (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
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ (∮ (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

Premises used: Complex.two_pi_I_ne_zero, mul_assoc, div_eq_mul_inv, div_eq_iff, mul_comm, 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 : ℕ
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)
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)
⊢ (PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) =
    (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]

Premises used: UpperHalfPlane.qExpansion, sub_zero, PowerSeries.coeff_mk, one_div_mul_eq_div, smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f_1 : F
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)).im

Tactic:
simpa using ht
-- 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)
⊢ 0 < R

Tactic:
have hR0 : 0 < R := Real.exp_pos _
-- 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
⊢ 0 < 2 * π * t

Tactic:
positivity
-- 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
⊢ -2 * π * t / h < 0

Tactic:
simpa [neg_div] using div_pos (by positivity) hh

Premises used: neg_div, div_pos
-- 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
⊢ R < 1

Tactic:
have hR1 : R < 1 := Real.exp_lt_one_iff.2 <| by simpa [neg_div] using div_pos (by positivity) hh
-- 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
⊢ 2 * π = h * (2 * π / h)

Tactic:
field_simp
-- 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
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 := ⋯ : ℍ }
⊢ (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 := ⋯ : ℍ }

Tactic:
rw [qExpansion_coeff_eq_circleIntegral hh hfper hfhol hfbdd n hR0 hR1, circleIntegral,
    show 2 * π = h * (2 * π / h) by field_simp]

Premises used: UpperHalfPlane.qExpansion_coeff_eq_circleIntegral, circleIntegral
-- 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
enter : 0
| (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 := ⋯ : ℍ }

Tactic:
enter [1, 2, 2]
-- 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
⊢ 0 = 0 * (2 * π / h)

Tactic:
simp
-- 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
rw : 0 * (2 * π / h)
| 0

Tactic:
rw [show 0 = 0 * (2 * π / h) by simp]
-- 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
enter : 0 * (2 * π / h)
| (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 := ⋯ : ℍ }

Tactic:
enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]
-- 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
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 := ⋯ : ℍ }
⊢ (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 := ⋯ : ℍ }

Tactic:
conv => enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]
-- 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
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 := ⋯ : ℍ }))
⊢ (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 := ⋯ : ℍ }

Tactic:
simp_rw [← intervalIntegral.smul_integral_comp_mul_right, real_smul, ← mul_assoc,
    ← intervalIntegral.integral_const_mul]

Premises used: Complex.real_smul, mul_assoc, intervalIntegral.smul_integral_comp_mul_right, intervalIntegral.integral_const_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
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 := ⋯ : ℍ })
⊢ 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 := ⋯ : ℍ }))

Tactic:
congr 1 with u
-- 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 : ℝ
⊢ 0 < ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ)).im

Tactic:
simpa using ht
-- 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 := ⋯ }
simp : cexp ((↑(-2 * π * t / h) : ℂ) + (↑(u * (2 * π / h)) : ℂ) * Complex.I) = 𝕢 h ((↑u : ℂ) + (↑t : ℂ) * (↑I : ℂ))
⊢ circleMap 0 R (u * (2 * π / h)) = 𝕢 h (↑τ : ℂ)

Tactic:
simp only [circleMap, ofReal_exp, ← exp_add, zero_add, τ, R]

Premises used: Complex.exp_add, circleMap, Complex.ofReal_exp, zero_add