awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
have h1 : Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
  (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k
Tactic: have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
      ext z
      ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ (↑(n ^ (l + k)) : ℝ)
have h0 : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: have h0 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =O[atTop] fun n ↦ ((n ^ k) : ℝ) := by
    have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
      ext z
      ring
    simpa [h1] using isBigO_ofReal_right.mp (Asymptotics.isBigO_const_mul_self
      ((2 * π * I / p) ^ k) (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)) atTop)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ (↑(n ^ (l + k)) : ℝ)
have push_cast : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (l + k)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
h0 :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ f n * (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k)
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (l + k)
have h : ∀ (x : ℕ), HPow.hPow (α := ℝ) (↑x : ℝ) (l + k) = HPow.hPow (α := ℝ) (↑x : ℝ) l * HPow.hPow (α := ℝ) (↑x : ℝ) k
Tactic: convert! hf.mul h0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ SummableLocallyUniformlyOn (α := ℂ)
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ))
    ℍₒ
have apply : ∀ K ⊆ ℍₒ,
  IsCompact K →
    ∃ (u : ℕ → ℝ),
      Summable u ∧
        ∀ (n : ℕ),
          ∀ k_1 ∈ K,
            ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                  (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
              u n
Tactic: apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ K,
          ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
            u n
have this : CompactSpace (↑K : Type)
Tactic: have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
⊢ ‖r‖ < 1
have simp : ∀ (x : (↑K : Type)), ‖cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))‖ < 1
Tactic: simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : (↑K : Type)
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))‖ < 1
have h1 : cexp (2 * (↑π : ℂ) * I * ((↑x : ℂ) / (↑p : ℂ))) = cexp (2 * (↑π : ℂ) * I * (↑x : ℂ) / (↑p : ℂ))
Tactic: have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ K,
          ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
            u n
have hr : ‖r‖ < 1
Tactic: have hr : ‖r‖ < 1 := by
    simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]
    intro x
    have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
    simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ K,
          ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
                (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) k_1‖ ≤
            u n
have refine : ∀ (n : ℕ) (z : ℂ) (hz : z ∈ K),
  ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n
Tactic: refine ⟨_, by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))), fun n z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
⊢ ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n
have h0 : norm (E := ℂ) ((mkOfCompact c : (a : (↑K : Type)) → ℂ) (Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z hz) : ℂ) ^ n ≤
  ‖mkOfCompact c‖ ^ n
Tactic: have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  norm (E := ℂ) ((mkOfCompact c : (a : (↑K : Type)) → ℂ) (Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z hz) : ℂ) ^ n ≤
    ‖mkOfCompact c‖ ^ n
⊢ ‖HSMul.hSMul (β := (x : ℂ) → ℂ) (f n)
        (iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * |r| ^ n
have simp : ∀
  (hr :
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := sorry :
          C((↑K : Type), ℂ) } <
      1),
  ‖f n‖ * ((2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖) ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := sorry :
            C((↑K : Type), ℂ) } ^
        n
Tactic: simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
    norm_natCast, abs_norm, ge_iff_le, r, c] at *
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
⊢ ‖f n‖ * ((2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖) ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
            C((↑K : Type), ℂ) } ^
        n
have rw : ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ ≤
  ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := sorry :
          C((↑K : Type), ℂ) } ^
      n
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
⊢ ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k * ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ ≤
    ‖f n‖ * (2 * |π| * (↑n : ℝ) / |p|) ^ k *
      norm (E := C((↑K : Type), ℂ))
          { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
            C((↑K : Type), ℂ) } ^
        n
have hbc : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ ≤
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := sorry :
        C((↑K : Type), ℂ) } ^
    n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
have h : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n
Tactic: convert! h0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n
have h : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n‖
Tactic: rw [← norm_pow, ← exp_nsmul']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace (↑K : Type)
c : C((↑K : Type), ℂ) :=
  { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 :
  ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n
hr :
  norm (E := C((↑K : Type), ℂ))
      { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
        C((↑K : Type), ℂ) } <
    1
h : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ)) ^ n‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n
have h₁ : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖
Tactic: rw [← norm_pow, ← exp_nsmul']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1
have simp : ∃ (c : ℝ) (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 ≤ c * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 1
Tactic: simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast,
      eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k b : ℕ
hb : 1 ≤ b
⊢ 1 ≤ 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 1
have norm_cast : 1 ≤ 1 * HPow.hPow (β := ℕ) b 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
⊢ SummableLocallyUniformlyOn (α := ℂ)
    (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ
have h0 : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1
Tactic: have h0 : (fun n : ℕ ↦ (1 : ℂ)) =O[atTop] fun n ↦ ((n ^ 1) : ℝ) := by
    simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast,
      eventually_atTop, ge_iff_le]
    exact ⟨1, 1, fun b hb ↦ by norm_cast; simp [hb]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
⊢ DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) r
have apply : DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) s
Tactic: apply DifferentiableOn.differentiableAt _ (hs.mem_nhds hr)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) s
have suffices : DifferentiableOn ℂ (F := ℂ) (iteratedDeriv a fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s
Tactic: suffices DifferentiableOn ℂ (iteratedDeriv a (fun z ↦ cexp (2 * π * I * z) ^ n)) s by
    apply this.congr (iteratedDerivWithin_of_isOpen hs)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
z : ℍ
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
have hsum : ∀ t ∈ ℍₒ, Summable (α := ℂ) fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * t) ^ n
Tactic: rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
z : ℍ
hsum : ∀ t ∈ ℍₒ, Summable (α := ℂ) fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * t) ^ n
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
have h : ∀ (k_1 : ℕ),
  1 ≤ k_1 →
    k_1 ≤ k →
      SummableLocallyUniformlyOn (α := ℂ)
        (fun (n : ℕ) ↦ iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ
Tactic: rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
z : ℍ
hsum : ∀ t ∈ ℍₒ, Summable (α := ℂ) fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * t) ^ n
h :
  ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k →
        SummableLocallyUniformlyOn (α := ℂ)
          (fun (n : ℕ) ↦ iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
have hf2 : ∀ (n k_1 : ℕ) (r : ℂ),
  k_1 ≤ k →
    r ∈ ℍₒ → DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) r
Tactic: rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ
      (↑z : ℂ) =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ)
have rw : -(2 * (↑π : ℂ) * I * iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ)) =
  -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ)
Tactic: rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
rw :
  -(2 * (↑π : ℂ) * I * iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ)) =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ)
⊢ iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ
      (↑z : ℂ) =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ)
have hf : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ)
Tactic: rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]