awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Eq (α := ℂ) (∑' (c : (↑(gammaSet 1 0 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑(0, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(0, c).2 : Fin 2 → ℤ) z)

Tactic:
simp [show ((0 : ℂ) ^ k)⁻¹ = 0 by aesop, eisSummand_of_gammaSet_eq_divIntMap]

Premises used: eisSummand_of_gammaSet_eq_divIntMap
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
b : ℕ
hb : b ≠ 0
⊢ NeZero b

Tactic:
have : NeZero b := ⟨hb⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
b : ℕ
hb : b ≠ 0
this : NeZero b
⊢ Eq (α := ℂ) (∑' (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z)

Tactic:
simpa [eisSummand_of_gammaSet_eq_divIntMap k z, tsum_mul_left, hb]
      using (gammaSetDivGcdEquiv b).tsum_eq (eisSummand k · z)

Premises used: Equiv.tsum_eq, tsum_mul_left, eisSummand_of_gammaSet_eq_divIntMap, Nat.cast, EisensteinSeries.eisSummand, EisensteinSeries.gammaSetDivGcdEquiv, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)

Tactic:
have HE1 := tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow hk hk2 z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (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 : ℕ)
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z

Tactic:
have HE2 := tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries hk z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (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 : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
norm_cast : 1 < k
⊢ 1 < Complex.re (↑k : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (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 : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
⊢ 1 < k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (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 : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
⊢ riemannZeta (↑k : ℂ) ≠ 0

Tactic:
have z2 : riemannZeta k ≠ 0 := riemannZeta_ne_zero_of_one_lt_re <| by norm_cast; grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (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 : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
z2 : riemannZeta (↑k : ℂ) ≠ 0
simp :
  ∀
    (HE1 :
      ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
        2 * riemannZeta (↑k : ℂ) +
          2 * ((-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ)) *
            ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
    (HE2 :
      (riemannZeta (↑k : ℂ))⁻¹ * ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
        ∑' (x : (↑(gammaSet 1 1 0) : Type)),
          (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹),
    HMul.hMul (α := ℂ) 2⁻¹
        (∑' (x : (↑(gammaSet 1 1 0) : Type)),
          (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹) =
      1 +
        (riemannZeta (↑k : ℂ))⁻¹ * (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
          ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
⊢ HSMul.hSMul (β := ℂ) (1 / 2) (∑' (x : (↑(gammaSet 1 1 0) : Type)), eisSummand (↑k : ℤ) (↑x : Fin 2 → ℤ) z) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)

Tactic:
simp [eisSummand, eisensteinSeries, ← inv_mul_eq_iff_eq_mul₀ z2] at HE1 HE2 ⊢

Premises used: inv_mul_eq_iff_eq_mul₀, EisensteinSeries.eisSummand, eisensteinSeries
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
z2 : riemannZeta (↑k : ℂ) ≠ 0
HE1 :
  ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
    2 * riemannZeta (↑k : ℂ) +
      2 * ((-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ)) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
HE2 :
  (riemannZeta (↑k : ℂ))⁻¹ * ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
    ∑' (x : (↑(gammaSet 1 1 0) : Type)), (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹
⊢ HMul.hMul (α := ℂ) 2⁻¹
      (∑' (x : (↑(gammaSet 1 1 0) : Type)),
        (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
⊢ k = 2 * (k / 2 - 1 + 1)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
⊢ k = 2 * (k / 2 - 1 + 1)

Tactic:
have h2 : k = 2 * (k / 2 - 1 + 1) := by grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
h2 : k = 2 * (k / 2 - 1 + 1)
⊢ let m := k / 2 - 1;
  k = 2 * (m + 1)

Tactic:
set m := k / 2 - 1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ m + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (2 * (m + 1))! = 2 * (m + 1) * (2 * m + 1)!

Tactic:
grind [Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ 2 * (m + 1) - 1 = 2 * m + 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
rw :
  (HPow.hPow (α := ℂ) (-1) (m + 1 + 1) * HPow.hPow (α := ℂ) 2 (2 * m + 1) * (↑π : ℂ) ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℂ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℂ))⁻¹ *
        (HPow.hPow (α := ℂ) (-2) (2 * (m + 1)) * (↑π : ℂ) ^ (2 * (m + 1)) * HPow.hPow (α := ℂ) (-1) (m + 1)) /
      (↑(2 * m + 1)! : ℂ) =
    -(2 * HMul.hMul (α := ℂ) 2 (↑(m + 1) : ℂ) / (↑(bernoulli (2 * (m + 1))) : ℂ))
⊢ (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) =
    -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))

Tactic:
rw [h2, Nat.cast_mul 2 (m + 1), Nat.cast_two, riemannZeta_two_mul_nat (show m + 1 ≠ 0 by grind),
    show (2 * (m + 1))! = 2 * (m + 1) * (2 * m + 1)! by grind [Nat.factorial_succ],
    show 2 * (m + 1) - 1 = 2 * m + 1 by grind, mul_pow, mul_pow, pow_mul I, I_sq]

Premises used: pow_mul, Nat.cast_mul, HAdd.hAdd, Complex.I_sq, OfNat.ofNat, mul_pow, riemannZeta_two_mul_nat, Nat.cast_two, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
norm_cast :
  ((↑(Int.negSucc 0 ^ (m + 1 + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * m + 1)) : ℤ)) : ℝ) * π ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℝ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℝ))⁻¹ *
        ((↑(Int.negSucc 1 ^ (2 * (m + 1))) : ℝ) * π ^ (2 * (m + 1)) * (↑(Int.negSucc 0 ^ (m + 1)) : ℝ)) /
      (↑(2 * m + 1)! : ℝ) =
    (↑(-((↑(2 * (2 * (m + 1))) : ℚ) / bernoulli (2 * (m + 1)))) : ℝ)
⊢ (HPow.hPow (α := ℂ) (-1) (m + 1 + 1) * HPow.hPow (α := ℂ) 2 (2 * m + 1) * (↑π : ℂ) ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℂ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℂ))⁻¹ *
        (HPow.hPow (α := ℂ) (-2) (2 * (m + 1)) * (↑π : ℂ) ^ (2 * (m + 1)) * HPow.hPow (α := ℂ) (-1) (m + 1)) /
      (↑(2 * m + 1)! : ℂ) =
    -(2 * HMul.hMul (α := ℂ) 2 (↑(m + 1) : ℂ) / (↑(bernoulli (2 * (m + 1))) : ℂ))

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
simp :
  HPow.hPow (α := ℝ) 2 (2 * (m + 1)) * HPow.hPow (α := ℝ) (-1) (m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ) =
    -(2 * HPow.hPow (α := ℝ) (-1) (m + 1 + 1) * HPow.hPow (α := ℝ) 2 (2 * m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ))
⊢ ((↑(Int.negSucc 0 ^ (m + 1 + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * m + 1)) : ℤ)) : ℝ) * π ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℝ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℝ))⁻¹ *
        ((↑(Int.negSucc 1 ^ (2 * (m + 1))) : ℝ) * π ^ (2 * (m + 1)) * (↑(Int.negSucc 0 ^ (m + 1)) : ℝ)) /
      (↑(2 * m + 1)! : ℝ) =
    (↑(-((↑(2 * (2 * (m + 1))) : ℚ) / bernoulli (2 * (m + 1)))) : ℝ)

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ HPow.hPow (α := ℝ) 2 (2 * (m + 1)) * HPow.hPow (α := ℝ) (-1) (m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ) =
    -(2 * HPow.hPow (α := ℝ) (-1) (m + 1 + 1) * HPow.hPow (α := ℝ) 2 (2 * m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ))

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (E hk : (a : ℍ) → ℂ) z =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)

Tactic:
q_expansion_riemannZeta hk hk2 z

Premises used: EisensteinSeries.q_expansion_riemannZeta
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
h :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
⊢ (E hk : (a : ℍ) → ℂ) z =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)

Tactic:
convert! q_expansion_riemannZeta hk hk2 z using 1

Premises used: EisensteinSeries.q_expansion_riemannZeta
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ k ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
h :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ)) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
h₁ :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
          ∑' (n : ℕ+),
            (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
              HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ))
h₂ h₃ :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
⊢ 1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)

Tactic:
rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]

Premises used: _private.0.eisensteinSeries_coeff_identity, sub_eq_add_neg, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
apply :
  ∀ (i : ℕ),
    ‖(↑((σ (k - 1) : (a : ℕ) → ℕ) i) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i‖ ≤
      ‖HPow.hPow (α := ℂ) (↑i : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i‖
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
apply Summable.of_norm_bounded
    (summable_norm_pow_mul_geometric_of_norm_lt_one k (norm_exp_two_pi_I_lt_one z))

Premises used: UpperHalfPlane.norm_exp_two_pi_I_lt_one, Summable.of_norm_bounded, summable_norm_pow_mul_geometric_of_norm_lt_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
simp :
  (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n
⊢ ‖(↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n‖ ≤
    ‖HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n‖

Tactic:
simp only [norm_mul, Complex.norm_natCast, norm_pow]

Premises used: norm_pow, Complex.norm_natCast, norm_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
hbc : (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) k
⊢ (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
e_a : k - 1 + 1 = k
⊢ n ^ (k - 1 + 1) = n ^ k

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ k - 1 + 1 = k

Tactic:
omega
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) k

Tactic:
exact_mod_cast (ArithmeticFunction.sigma_le_pow_succ (k - 1) n).trans_eq (by congr 1; omega)

Premises used: LE.le.trans_eq, HSub.hSub, ArithmeticFunction.sigma_le_pow_succ, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
set :
  let β := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ));
  (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) =
    if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
⊢ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) =
    if m = 0 then 1 else -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ)) * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)

Tactic:
set β : ℂ := -(2 * k / bernoulli k : ℂ)

Premises used: HMul.hMul, bernoulli, HDiv.hDiv, Rat.cast, Nat.cast, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
suffices : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 1 (↑τ : ℂ) ^ m) ((E hk : (a : ℍ) → ℂ) τ : ℂ)
⊢ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) =
    if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)

Tactic:
suffices ∀ τ : ℍ, HasSum (fun m ↦ c m • 𝕢 (1 : ℝ) τ ^ m) (E hk τ) from
    (ModularFormClass.qExpansion_coeff_unique one_pos one_mem_strictPeriods_SL this m).symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
⊢ 1 ≤ k

Tactic:
omega
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)

Tactic:
have hS : Summable fun n : ℕ ↦ (σ (k - 1) (n + 1) : ℂ) * cexp (2 * π * I * τ) ^ (n + 1) :=
    (summable_nat_add_iff 1).mpr (summable_sigma_mul_cexp_pow (by omega) τ)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
rw :
  HasSum (fun (n : ℕ) ↦ c (n + 1) • 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (∑ i ∈ Finset.range 1, c i • 𝕢 1 (↑τ : ℂ) ^ i : ℂ))
⊢ HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 1 (↑τ : ℂ) ^ m) ((E hk : (a : ℍ) → ℂ) τ : ℂ)

Tactic:
rw [← hasSum_nat_add_iff' 1]

Premises used: hasSum_nat_add_iff', OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
simp :
  HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ))
⊢ HasSum (fun (n : ℕ) ↦ c (n + 1) • 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (∑ i ∈ Finset.range 1, c i • 𝕢 1 (↑τ : ℂ) ^ i : ℂ))

Tactic:
simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, smul_eq_mul, Finset.range_one,
    ite_mul, one_mul, Finset.sum_singleton, pow_zero, c]

Premises used: pow_zero, Finset.sum_singleton, ite_mul, reduceIte, Finset.range_one, and_false, smul_eq_mul, one_ne_zero, Nat.add_eq_zero_iff, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ))) (↑(↑n : ℕ) : ℤ)

Tactic:
have := q_expansion_bernoulli hk hk2 τ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
this :
  (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ))) (↑(↑n : ℕ) : ℤ)
⊢ (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)

Tactic:
simp_rw [zpow_natCast] at this

Premises used: zpow_natCast