awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
hbc :
  ‖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
⊢ ‖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

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 * z / (↑p : ℂ))‖ ^ n ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n

Tactic:
h0
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℂ))‖ ≤
    norm (E := C((↑K : Type), ℂ))
        { toFun := fun (r : (↑K : Type)) ↦ cexp (2 * (↑π : ℂ) * I * (↑r : ℂ) / (↑p : ℂ)), continuous_toFun := ⋯ :
          C((↑K : Type), ℂ) } ^
      n

Tactic:
convert! h0
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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‖
h₁ h₂ : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z / (↑p : ℂ))‖ = ‖cexp (2 * (↑π : ℂ) * I * z / (↑p : ℂ))‖ ^ n

Tactic:
rw [← norm_pow, ← exp_nsmul']

Premises used: norm_pow, Complex.exp_nsmul'
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
simp : ∃ (c : ℝ) (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 ≤ c * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 1
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1

Tactic:
simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast,
      eventually_atTop, ge_iff_le]

Premises used: norm_pow, Real.norm_natCast, ge_iff_le, Asymptotics.isBigO_iff, NormOneClass.norm_one, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k b : ℕ
hb : 1 ≤ b
norm_cast : 1 ≤ 1 * HPow.hPow (β := ℕ) b 1
⊢ 1 ≤ 1 * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k b : ℕ
hb : 1 ≤ b
⊢ 1 ≤ 1 * HPow.hPow (β := ℕ) b 1

Tactic:
simp [hb]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
⊢ ∃ (c : ℝ) (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 ≤ c * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 1

Tactic:
exact ⟨1, 1, fun b hb ↦ by norm_cast; simp [hb]⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
⊢ 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]⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
h0 : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1
⊢ LT.lt (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
h0 : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1
⊢ SummableLocallyUniformlyOn (α := ℂ)
    (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
simpa using summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp k 1 (p := 1)
    (by norm_num) h0

Premises used: OfNat.ofNat, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
apply : DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) s
⊢ DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) r

Tactic:
apply DifferentiableOn.differentiableAt _ (hs.mem_nhds hr)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
this : DifferentiableOn ℂ (F := ℂ) (iteratedDeriv a fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) s

Tactic:
apply this.congr (iteratedDerivWithin_of_isOpen hs)

Premises used: DifferentiableOn.congr, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
suffices : DifferentiableOn ℂ (F := ℂ) (iteratedDeriv a fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin a (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s) s

Tactic:
suffices DifferentiableOn ℂ (iteratedDeriv a (fun z ↦ cexp (2 * π * I * z) ^ n)) s by
    apply this.congr (iteratedDerivWithin_of_isOpen hs)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDeriv a fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) s

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ (↑z : ℂ) ∈ ℍₒ

Tactic:
simpa using z.2

Premises used: UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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) ℍₒ) ℍₒ
hf2 :
  ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k →
      r ∈ ℍₒ →
        DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) r
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))

Tactic:
rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]

Premises used: iteratedDerivWithin_tsum, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ t ∈ ℍₒ, Summable (α := ℂ) fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * t) ^ n

Tactic:
fun x hx ↦ summable_geometric_iff_norm_lt_one.mpr
      (UpperHalfPlane.norm_exp_two_pi_I_lt_one ⟨x, hx⟩)

Premises used: Iff.mpr, UpperHalfPlane.norm_exp_two_pi_I_lt_one, UpperHalfPlane.mk, summable_geometric_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ t ∈ ℍₒ, Summable (α := ℂ) fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * t) ^ n

Tactic:
exact fun x hx ↦ summable_geometric_iff_norm_lt_one.mpr
      (UpperHalfPlane.norm_exp_two_pi_I_lt_one ⟨x, hx⟩)

Premises used: Iff.mpr, UpperHalfPlane.norm_exp_two_pi_I_lt_one, UpperHalfPlane.mk, summable_geometric_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k →
        SummableLocallyUniformlyOn (α := ℂ)
          (fun (n : ℕ) ↦ iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n

Premises used: summableLocallyUniformlyOn_iteratedDerivWithin_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k →
        SummableLocallyUniformlyOn (α := ℂ)
          (fun (n : ℕ) ↦ iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
exact fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n

Premises used: summableLocallyUniformlyOn_iteratedDerivWithin_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k →
      r ∈ ℍₒ →
        DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) r

Tactic:
fun n l z hl hz ↦ differentiableAt_iteratedDerivWithin_cexp n l
      isOpen_upperHalfPlaneSet hz

Premises used: UpperHalfPlane.isOpen_upperHalfPlaneSet, differentiableAt_iteratedDerivWithin_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k →
      r ∈ ℍₒ →
        DifferentiableAt ℂ (F := ℂ) (iteratedDerivWithin k_1 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ) r

Tactic:
exact fun n l z hl hz ↦ differentiableAt_iteratedDerivWithin_cexp n l
      isOpen_upperHalfPlaneSet hz

Premises used: UpperHalfPlane.isOpen_upperHalfPlaneSet, differentiableAt_iteratedDerivWithin_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ∞
⊢ ContDiffOn ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ

Tactic:
contDiffOn_of_differentiableOn_deriv fun m _ z hz ↦
  (((summableLocallyUniformlyOn_iteratedDerivWithin_cexp m).differentiableOn
  isOpen_upperHalfPlaneSet (fun n _ hz ↦ differentiableAt_iteratedDerivWithin_cexp n m
  isOpen_upperHalfPlaneSet hz)) z hz).congr (fun z hz ↦ iteratedDerivWithin_tsum_cexp_eq m ⟨z, hz⟩)
  (iteratedDerivWithin_tsum_cexp_eq m ⟨z, hz⟩)

Premises used: summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_tsum_cexp_eq, DifferentiableWithinAt.congr, UpperHalfPlane.mk, contDiffOn_of_differentiableOn_deriv, SummableLocallyUniformlyOn.differentiableOn, UpperHalfPlane.isOpen_upperHalfPlaneSet, differentiableAt_iteratedDerivWithin_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (↑z : ℂ) ∈ ℍₒ

Tactic:
simpa using z.2

Premises used: UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℂ)
hf :
  ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ 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 : ℂ)

Tactic:
rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]

Premises used: iteratedDerivWithin_const_sub, IsOpen.uniqueDiffOn, iteratedDerivWithin_const_mul, UpperHalfPlane.isOpen_upperHalfPlaneSet, iteratedDerivWithin_fun_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ -(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:
simp only [iteratedDerivWithin_tsum_cexp_eq, neg_mul]

Premises used: iteratedDerivWithin_tsum_cexp_eq, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ (↑z : ℂ)

Tactic:
exact (contDiffOn_tsum_cexp k).contDiffWithinAt (by simpa using z.2)

Premises used: Nat.cast, contDiffOn_tsum_cexp, ContDiffOn.contDiffWithinAt
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℂ)

Tactic:
have : 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 := by
    rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]
    · simp only [iteratedDerivWithin_tsum_cexp_eq, neg_mul]
    · exact (contDiffOn_tsum_cexp k).contDiffWithinAt (by simpa using z.2)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
simp_rw :
  Eq (α := ℂ)
    (∑' (x : ℕ),
      -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
        (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
    (∑' (x : ℕ), -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
⊢ -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
simp_rw [← tsum_mul_left]

Premises used: tsum_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
e_f :
  Eq (α := ℕ → ℂ)
    (fun (x : ℕ) ↦
      -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
        (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
    fun (x : ℕ) ↦ -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)
⊢ Eq (α := ℂ)
    (∑' (x : ℕ),
      -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
        (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
    (∑' (x : ℕ), -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
e_f :
  ∀ (y : ℕ),
    -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
        (HPow.hPow (α := ℂ) (↑y : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ y) =
      -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑y : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ y)
⊢ Eq (α := ℕ → ℂ)
    (fun (x : ℕ) ↦
      -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
        (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
    fun (x : ℕ) ↦ -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)

Tactic:
ext y
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
y : ℕ
⊢ -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
      (HPow.hPow (α := ℂ) (↑y : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ y) =
    -(2 * (↑π : ℂ) * I) * ((2 * (↑π : ℂ) * I * (↑y : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ y)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
⊢ -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
have h : -(2 * π * I * (2 * π * I) ^ k) * ∑' (n : ℕ), n ^ k * cexp (2 * π * I * z) ^ n =
        -(2 * π * I) * ∑' n : ℕ, (2 * π * I * n) ^ k * cexp (2 * π * I * z) ^ n := by
    simp_rw [← tsum_mul_left]
    congr
    ext y
    ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
h :
  -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
simp :
  Eq (α := ℂ) (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
⊢ iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n) ℍₒ
      (↑z : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
simp only [this, neg_mul, pow_succ', h, neg_inj, mul_eq_mul_left_iff, mul_eq_zero,
    OfNat.ofNat_ne_zero, ofReal_eq_zero, Real.pi_ne_zero, or_self, I_ne_zero, or_false]

Premises used: OfNat.ofNat_ne_zero, mul_eq_mul_left_iff, Complex.I_ne_zero, mul_eq_zero, Complex.ofReal_eq_zero, neg_inj, or_self, neg_mul, or_false, pow_succ', Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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 : ℂ)
h :
  -(2 * (↑π : ℂ) * I * (2 * (↑π : ℂ) * I) ^ k) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n =
    -(2 * (↑π : ℂ) * I) * ∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
e_f :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
    fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
⊢ Eq (α := ℂ) (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)

Tactic:
congr