awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (n : ℕ),
    iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ) =
      (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

Tactic:
ext n
-- 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
n : ℕ
⊢ ∀ (x : ℂ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * x / 1) = cexp (2 * (↑π : ℂ) * I * x / 1) ^ n

Tactic:
have := exp_nsmul' (p := 1) (a := 2 * π * I) (n := n)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
⊢ ∀ (x : ℂ), cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * x) = cexp (2 * (↑π : ℂ) * I * x) ^ n

Tactic:
simp_rw [div_one] at this

Premises used: div_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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) = cexp (2 * (↑π : ℂ) * I * x) ^ n
⊢ iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * s) ^ n) ℍₒ (↑z : ℂ) =
    (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
simpa [this, UpperHalfPlane.coe] using
    iteratedDerivWithin_cexp_aux k n 1 isOpen_upperHalfPlaneSet z.2

Premises used: UpperHalfPlane.coe, _private.0.iteratedDerivWithin_cexp_aux, OfNat.ofNat, UpperHalfPlane.coe_im_pos, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
rw :
  Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ (↑z : ℂ))
    (iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n)
      ℍₒ (↑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

Tactic:
rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]

Premises used: iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, _private.0.iteratedDerivWithin_tsum_exp_aux_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
x : ℂ
hx : x ∈ ℍₒ
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * x) ^ n

Tactic:
simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩

Premises used: UpperHalfPlane.mk, pi_mul_cot_pi_q_exp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ (↑z : ℂ))
    (iteratedDerivWithin k (fun (z : ℂ) ↦ (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * z) ^ n)
      ℍₒ (↑z : ℂ))

Tactic:
exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩))
      (by simpa using z.2)

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

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)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) ≠ 0

Tactic:
simp [Nat.factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
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))
⊢ ∑' (n : ℤ), 1 / ((↑z : ℂ) + (↑n : ℂ)) ^ (k + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k + 1) / (↑k ! : ℂ) *
      ∑' (n : ℕ), HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
simp_rw [(eq_inv_mul_iff_mul_eq₀ (by simp [Nat.factorial_ne_zero])).mpr this, ← tsum_mul_left]

Premises used: Iff.mpr, tsum_mul_left, eq_inv_mul_iff_mul_eq₀
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
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)
⊢ 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:
congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
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)
⊢ 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:
ext n
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ
rw : (-2 * (↑π : ℂ) * I) ^ (k + 1) = (-(2 * (↑π : ℂ) * I)) ^ (k + 1)
⊢ (-2 * (↑π : ℂ) * I) ^ (k + 1) = HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ) * I) ^ (k + 1)

Tactic:
rw [← neg_pow]

Premises used: neg_pow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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) = (-(2 * (↑π : ℂ) * I)) ^ (k + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ
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)
⊢ (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:
rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ
e_f :
  -(HPow.hPow (α := ℂ) (↑n : ℂ) k / (↑k ! : ℂ)) =
    HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) (k + 1) / (↑k ! : ℂ)
⊢ (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:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ
e_f :
  -(HPow.hPow (α := ℂ) (↑n : ℂ) k * (↑k ! : ℂ)⁻¹) =
    -(HPow.hPow (α := ℂ) (↑n : ℂ) k * (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (-1) (k * 2))
⊢ -(HPow.hPow (α := ℂ) (↑n : ℂ) k / (↑k ! : ℂ)) =
    HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) (k + 1) / (↑k ! : ℂ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 (α := ℂ) (↑n : ℂ) k * (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (-1) (k * 2))

Tactic:
simp [Nat.mul_two]

Premises used: Nat.mul_two
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
⊢ 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im

Tactic:
simpa using z.2

Premises used: UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
⊢ 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im

Tactic:
have he : 0 < (e * (z : ℂ)).im := by
    simpa using z.2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
⊢ LT.lt (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) k) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
simp [← Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl]

Premises used: Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
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
⊢ Summable (α := ℂ) fun (c : ℕ) ↦
    HPow.hPow (α := ℂ) (↑c : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑e : ℕ) : ℂ) * (↑z : ℂ)) ^ c

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

Premises used: SummableLocallyUniformlyOn.summable, Summable.congr, OfNat.ofNat, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
e : ℕ+
z : ℍ
he : 0 < ((↑(↑e : ℕ) : ℂ) * (↑z : ℂ)).im
⊢ ∀ (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:
grind [ofReal_one, iteratedDerivWithin_zero, Pi.smul_apply, smul_eq_mul]

Premises used: Complex.ofReal_one, iteratedDerivWithin_zero, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
rw₁ : Summable (α := ℂ) fun (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 : ℕ)

Tactic:
rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]

Premises used: tsum_zero_pnat_eq_tsum_nat, EisensteinSeries.qExpansion_identity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ k ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (-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:
simp [show k ≠ 0 by grind]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
apply :
  ∀ (b : ℕ),
    HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑1 : ℕ) : ℂ) * (↑z : ℂ)) ^ b =
      HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ b
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
apply (summable_pow_mul_cexp k 1 z).congr

Premises used: Summable.congr, OfNat.ofNat, summable_pow_mul_cexp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∀ (b : ℕ),
    HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑(↑1 : ℕ) : ℂ) * (↑z : ℂ)) ^ b =
      HPow.hPow (α := ℂ) (↑b : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ b

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ Summable (α := ℂ) fun (x : Fin 2 → ℤ) ↦ eisSummand (↑k : ℤ) x z

Tactic:
summable_norm_iff.mp <| summable_norm_eisSummand (Int.toNat_le.mp hk) z

Premises used: EisensteinSeries.summable_norm_eisSummand, Int.toNat_le, Iff.mp, summable_norm_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ Summable (α := ℂ) fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z

Tactic:
(finTwoArrowEquiv ℤ).summable_iff.mp <| (summable_eisSummand hk z).congr (fun v ↦ ?_)

Premises used: summable_eisSummand, Int, Equiv.summable_iff, Iff.mp, Summable.congr, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
refine :
  ∀ (v : Fin 2 → ℤ),
    eisSummand (↑k : ℤ) v z =
      ((fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z) ∘ (⇑(finTwoArrowEquiv ℤ) : (a : Fin 2 → ℤ) → ℤ × ℤ)) v
⊢ Summable (α := ℂ) fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z

Tactic:
refine (finTwoArrowEquiv ℤ).summable_iff.mp <| (summable_eisSummand hk z).congr (fun v ↦ ?_)

Premises used: summable_eisSummand, Int, Equiv.summable_iff, Iff.mp, Summable.congr, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
v : Fin 2 → ℤ
⊢ eisSummand (↑k : ℤ) v z =
    ((fun (x : ℤ × ℤ) ↦ eisSummand (↑k : ℤ) ![x.1, x.2] z) ∘ (⇑(finTwoArrowEquiv ℤ) : (a : Fin 2 → ℤ) → ℤ × ℤ)) v

Tactic:
simp [show ![v 0, v 1] = v from List.ofFn_inj.mp rfl]

Premises used: List.ofFn_inj, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ Summable (α := ℂ) fun (b : ℤ) ↦ ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(b, c).1, (b, c).2] z

Tactic:
simpa using (summable_prod_eisSummand hk z).prod

Premises used: Summable.prod, summable_prod_eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
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 : ℕ)
rw₁ :
  ∀ (n : ℤ),
    Eq (α := ℂ) (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(-n, c).1, (-n, c).2] z)
      (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] 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 : ℕ)

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)]

Premises used: Equiv.tsum_eq, Int, finTwoArrowEquiv_symm_apply, tsum_int_eq_zero_add_two_mul_tsum_pnat, Summable.tsum_prod, summable_prod_eisSummand, Equiv.symm, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
nth_rewrite :
  Eq (α := ℂ) (∑' (d : ℤ), eisSummand (↑k : ℤ) ![(-n, -d).1, (-n, -d).2] z)
    (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)
⊢ Eq (α := ℂ) (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(-n, c).1, (-n, c).2] z)
    (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)

Tactic:
nth_rewrite 1 [← tsum_comp_neg]

Premises used: tsum_comp_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n y : ℤ
⊢ eisSummand (↑k : ℤ) ![(-n, -y).1, (-n, -y).2] z = eisSummand (↑k : ℤ) ![(n, y).1, (n, y).2] z

Tactic:
simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]

Premises used: neg_add_rev, Int.cast, Even.neg_pow, neg_add, EisensteinSeries.eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ Eq (α := ℂ) (∑' (d : ℤ), eisSummand (↑k : ℤ) ![(-n, -d).1, (-n, -d).2] z)
    (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)

Tactic:
exact tsum_congr fun y ↦ by simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ Eq (α := ℂ) (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(-n, c).1, (-n, c).2] z)
    (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)

Tactic:
case h₁ =>
    nth_rewrite 1 [← tsum_comp_neg]
    exact tsum_congr fun y ↦ by simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]

Premises used: tsum_congr, tsum_comp_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 1 ≤ k - 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 0 < ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ)).im

Tactic:
simpa using z.2

Premises used: UpperHalfPlane.coe_im_pos