awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ 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
have 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 : ℂ)
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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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
have 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))
Tactic: simp_rw [← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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 : ℂ)
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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 : ℂ)
⊢ 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)
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
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 : ℂ)
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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
⊢ 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
have simp : Eq (α := ℂ) (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
  (∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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
⊢ Eq (α := ℂ) (∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
    (∑' (n : ℕ), (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ))
    fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have e_f : ∀ (n : ℕ),
  iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ) =
    (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
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
n : ℕ
⊢ iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ) =
    (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have this₁ : ∀ (x : ℂ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * x / 1) = cexp (2 * (↑π : ℂ) * I * x / 1) ^ n
Tactic: have := exp_nsmul' (p := 1) (a := 2 * π * I) (n := n)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this_1 :
  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
n : ℕ
this : ∀ (x : ℂ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * x / 1) = cexp (2 * (↑π : ℂ) * I * x / 1) ^ n
⊢ iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ) =
    (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have this₁ : ∀ (x : ℂ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * x) = cexp (2 * (↑π : ℂ) * I * x) ^ n
Tactic: simp_rw [div_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have rw : Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ (↑z : ℂ))
  (iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n)
    ℍₒ (↑z : ℂ))
Tactic: rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have this : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
  -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
Tactic: have : (-1) ^ k * k ! * ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
    -(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
    rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
    exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩))
      (by simpa using z.2)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
⊢ ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have simp_rw : Eq (α := ℂ)
  (∑' (x : ℕ),
    (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
      (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)))
  (∑' (x : ℕ),
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
Tactic: simp_rw [(eq_inv_mul_iff_mul_eq₀ (by simp [Nat.factorial_ne_zero])).mpr this, ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
⊢ Eq (α := ℂ)
    (∑' (x : ℕ),
      (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
        (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)))
    (∑' (x : ℕ),
      (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
        (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x))
have e_f : Eq (α := ℕ → ℂ)
  (fun (x : ℕ) ↦
    (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
      (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)))
  fun (x : ℕ) ↦
  (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) * (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
⊢ Eq (α := ℕ → ℂ)
    (fun (x : ℕ) ↦
      (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
        (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)))
    fun (x : ℕ) ↦
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑x : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ x)
have e_f : ∀ (n : ℕ),
  (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
      (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
n : ℕ
⊢ (-2 * (↑π : ℂ) * I) ^ (k + 1) = HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ) * I) ^ (k + 1)
have rw : (-2 * (↑π : ℂ) * I) ^ (k + 1) = (-(2 * (↑π : ℂ) * I)) ^ (k + 1)
Tactic: rw [← neg_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
n : ℕ
⊢ (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
      (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
have e_f : (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
    (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
    (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
Tactic: rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
n : ℕ
⊢ (HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ))⁻¹ *
      (-(2 * (↑π : ℂ) * I) ^ (k + 1) * (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n)
have e_f : -(HPow.hPow (α := ℂ) (↑n : ℂ) k / (↑k ! : ℂ)) =
  HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) (k + 1) / (↑k ! : ℂ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    -(2 * (↑π : ℂ) * I) ^ (k + 1) * ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
n : ℕ
⊢ -(HPow.hPow (α := ℂ) (↑n : ℂ) k / (↑k ! : ℂ)) =
    HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) (k + 1) / (↑k ! : ℂ)
have e_f : -(HPow.hPow (α := ℂ) (↑n : ℂ) k * (↑k ! : ℂ)⁻¹) =
  -(HPow.hPow (α := ℂ) (↑n : ℂ) k * (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (-1) (k * 2))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
e : ℕ+
z : ℍ
⊢ Summable (α := ℂ) fun (c : ℕ) ↦
    HPow.hPow (α := ℂ) (↑c : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑e : ℕ) : ℂ) * (↑z : ℂ)) ^ c
have he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
Tactic: have he : 0 < (e * (z : ℂ)).im := by
    simpa using z.2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
e : ℕ+
z : ℍ
he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
⊢ Summable (α := ℂ) fun (c : ℕ) ↦
    HPow.hPow (α := ℂ) (↑c : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑e : ℕ) : ℂ) * (↑z : ℂ)) ^ c
have apply : ∀ (b : ℕ),
  HSMul.hSMul (β := (x : ℂ) → ℂ) (HPow.hPow (α := ℂ) (↑b : ℂ) k)
      (iteratedDerivWithin 0 (fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑1 : ℂ)) ^ b) ℍₒ)
      ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)) =
    HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑e : ℕ) : ℂ) * (↑z : ℂ)) ^ b
Tactic: apply ((summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp 0 k (p := 1)
    (f := fun n ↦ (n ^ k : ℂ)) (by norm_num)
    (by simp [← Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl])).summable he).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
have rw : (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
    (HPow.hPow (α := ℂ) (↑0 : ℂ) k * HPow.hPow (β := ℕ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) 0 +
      ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)) =
  (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
    ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
Tactic: rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
rw :
  (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      (HPow.hPow (α := ℂ) (↑0 : ℂ) k * HPow.hPow (β := ℕ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) 0 +
        ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
⊢ ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ+), HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
have rw₁ : Summable (α := ℂ) fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
Tactic: rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have apply : ∀ (b : ℕ),
  HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑1 : ℕ) : ℂ) * (↑z : ℂ)) ^ b =
    HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ b
Tactic: apply (summable_pow_mul_cexp k 1 z).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ Summable (α := ℂ) fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z
have refine : ∀ (v : Fin 2 → ℤ),
  eisSummand (↑k : ℤ) v z =
    ((fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z) ∘ (⇑(finTwoArrowEquiv ℤ) : (a : Fin 2 → ℤ) → ℤ × ℤ)) v
Tactic: refine (finTwoArrowEquiv ℤ).summable_iff.mp <| (summable_eisSummand hk z).congr (fun v ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z =
    2 * riemannZeta (↑k : ℂ) +
      2 * ((-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ)) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
have rw : ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z +
    HSMul.hSMul (α := ℕ) (β := ℂ) 2
      (∑' (n : ℕ+) (c : ℤ), eisSummand (↑k : ℤ) ![((↑(↑n : ℕ) : ℤ), c).1, ((↑(↑n : ℕ) : ℤ), c).2] z) =
  2 * riemannZeta (↑k : ℂ) +
    2 * ((-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ)) *
      ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
Tactic: rw [← (finTwoArrowEquiv ℤ).symm.tsum_eq, finTwoArrowEquiv_symm_apply,
    Summable.tsum_prod (summable_prod_eisSummand hk z),
    tsum_int_eq_zero_add_two_mul_tsum_pnat (fun n ↦ ?h₁)
      (by simpa using (summable_prod_eisSummand hk z).prod)]