awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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 : ℕ)
⊢ ∑' (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₁ : ∀ (n : ℤ),
  Eq (α := ℂ) (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(-n, c).1, (-n, c).2] z)
    (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
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)
have nth_rewrite : Eq (α := ℂ) (∑' (d : ℤ), eisSummand (↑k : ℤ) ![(-n, -d).1, (-n, -d).2] z)
  (∑' (c : ℤ), eisSummand (↑k : ℤ) ![(n, c).1, (n, c).2] z)
Tactic: nth_rewrite 1 [← tsum_comp_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (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 : ℕ)
have H : ∀ (b : ℕ+),
  ∑' (n : ℤ), 1 / ((↑{ coe := (↑(↑b : ℕ) : ℂ) * (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ) + (↑n : ℂ)) ^ (k - 1 + 1) =
    (-2 * (↑π : ℂ) * I) ^ (k - 1 + 1) / (↑(k - 1)! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
          cexp (2 * (↑π : ℂ) * I * (↑{ coe := (↑(↑b : ℕ) : ℂ) * (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^ (↑n : ℕ)
Tactic: have H (b : ℕ+) := qExpansion_identity_pnat (k := k - 1) (by grind) ⟨b * z, by simpa using z.2⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), 1 / ((↑{ coe := (↑(↑b : ℕ) : ℂ) * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) + (↑n : ℂ)) ^ (k - 1 + 1) =
      (-2 * (↑π : ℂ) * I) ^ (k - 1 + 1) / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
            cexp (2 * (↑π : ℂ) * I * (↑{ coe := (↑(↑b : ℕ) : ℂ) * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ (↑n : ℕ)
⊢ ∑' (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 : ℕ)
have H₁ : ∀ (b : ℕ+),
  ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
    (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
Tactic: simp_rw [show k - 1 + 1 = k by grind, one_div] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ ∑' (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 : ℕ)
have H₁ : ∀ (b : ℕ+),
  ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
    (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
Tactic: simp only [neg_mul] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ ∑' (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 : ℕ)
have rw : ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z +
    HMul.hMul (α := ℂ) (↑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 [nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z +
      HMul.hMul (α := ℂ) (↑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 : ℕ))
have e_a : ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z = 2 * riemannZeta (↑k : ℂ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
e_a : ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z = 2 * riemannZeta (↑k : ℂ)
⊢ ∑' (c : ℤ), eisSummand (↑k : ℤ) ![(0, c).1, (0, c).2] z +
      HMul.hMul (α := ℂ) (↑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 : ℕ))
have e_a₁ : ∑' (n : ℕ+) (c : ℤ), eisSummand (↑k : ℤ) ![((↑(↑n : ℕ) : ℤ), c).1, ((↑(↑n : ℕ) : ℤ), c).2] z =
  (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
    ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand (↑k : ℤ) ![((↑(↑n : ℕ) : ℤ), c).1, ((↑(↑n : ℕ) : ℤ), c).2] z =
    (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
      ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
have e_a : Eq (α := ℂ)
  (∑' (m : ℕ+) (n : ℕ+),
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ))
  (∑' (m : ℕ+) (n : ℕ+),
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑m : ℕ) * (↑n : ℕ)))
Tactic: suffices ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * (m * z)) ^ (n : ℕ) =
        ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * z) ^ (m * n : ℕ) by
      simp [eisSummand, H, tsum_mul_left,
        ← tsum_prod_pow_eq_tsum_sigma (k - 1) (norm_exp_two_pi_I_lt_one z), this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ Eq (α := ℂ)
    (∑' (m : ℕ+) (n : ℕ+),
      HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ))
    (∑' (m : ℕ+) (n : ℕ+),
      HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑m : ℕ) * (↑n : ℕ)))
have e_a : Eq (α := ℂ)
  (∑' (m : ℕ+) (n : ℕ+),
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
      cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)))))
  (∑' (m : ℕ+) (n : ℕ+),
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp ((↑((↑m : ℕ) * (↑n : ℕ)) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ))))
Tactic: simp_rw [← Complex.exp_nat_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), (((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ k)⁻¹ =
      (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
m n : ℕ+
⊢ HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
      cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)))) =
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp ((↑((↑m : ℕ) * (↑n : ℕ)) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ)))
have push_cast : HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
    cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)))) =
  HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
    cexp (HMul.hMul (α := ℂ) (↑(↑m : ℕ) : ℂ) (↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℤ
z : ℍ
n : ℕ
v : (↑(gammaSet 1 n 0) : Type)
⊢ ((↑((↑v : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑v : Fin 2 → ℤ) 1) : ℂ)) ^ (-k) =
    (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹ *
      ((↑(divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑(divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ) 1) : ℂ)) ^
        (-k)
have nth_rw : ((↑((n • divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ)) 0) : ℂ) * (↑z : ℂ) +
      (↑((n • divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ)) 1) : ℂ)) ^
    (-k) =
  (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹ *
    ((↑(divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑(divIntMap (↑n : ℤ) (↑v : Fin 2 → ℤ) 1) : ℂ)) ^ (-k)
Tactic: nth_rw 1 2 [gammaSet_eq_gcd_mul_divIntMap v.2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
have hk1 : 1 < k
Tactic: have hk1 : 1 < k := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
have hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
Tactic: have hk2 : 3 ≤ (k : ℤ) := mod_cast hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
have simp_rw : ∑' (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)),
    eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z =
  riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
Tactic: simp_rw [← gammaSetDivGcdSigmaEquiv.symm.tsum_eq, gammaSetDivGcdSigmaEquiv_symm_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ ∑' (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)),
      eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z =
    riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
have rw : Eq (α := ℂ)
  (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)),
    eisSummand (↑k : ℤ)
      (↑(Sigma.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))
            (Sigma.mk (β := fun (b : ℕ) ↦ (↑(gammaSet 1 b 0) : Type)) b c)) :
        Fin 2 → ℤ)
      z)
  (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
    1 / HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
Tactic: rw [eisensteinSeries, Summable.tsum_sigma ?hsumm, zeta_nat_eq_tsum_of_gt_one hk1,
    tsum_mul_tsum_of_summable_norm (by simp [hk1]) ((summable_norm_eisSummand hk2 z).subtype _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
rw :
  Eq (α := ℂ)
    (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)),
      eisSummand (↑k : ℤ)
        (↑(Sigma.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))
              (Sigma.mk (β := fun (b : ℕ) ↦ (↑(gammaSet 1 b 0) : Type)) b c)) :
          Fin 2 → ℤ)
        z)
    (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      1 / HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
⊢ ∑' (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)),
      eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z =
    riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
have rw₁ : Summable (α := ℂ) fun (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)) ↦
  eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z
Tactic: rw [eisensteinSeries, Summable.tsum_sigma ?hsumm, zeta_nat_eq_tsum_of_gt_one hk1,
    tsum_mul_tsum_of_summable_norm (by simp [hk1]) ((summable_norm_eisSummand hk2 z).subtype _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Eq (α := ℂ)
    (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)),
      eisSummand (↑k : ℤ)
        (↑(Sigma.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))
              (Sigma.mk (β := fun (b : ℕ) ↦ (↑(gammaSet 1 b 0) : Type)) b c)) :
          Fin 2 → ℤ)
        z)
    (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      1 / HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
have simp_rw : Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
  (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
    (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
have rw : Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
  (∑' (b : ℕ) (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
    (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z)
Tactic: rw [Summable.tsum_prod' ?h₁ fun b ↦ ?h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
rw :
  Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (b : ℕ) (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z)
⊢ Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
have rw₁ : Summable (α := ℂ) fun (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }) ↦
  (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z
Tactic: rw [Summable.tsum_prod' ?h₁ fun b ↦ ?h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
rw :
  Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (b : ℕ) (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z)
rw₁ :
  Summable (α := ℂ) fun (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }) ↦
    (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z
⊢ Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (z_1 : ℕ × { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑z_1.1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑z_1.2 : Fin 2 → ℤ) z)
have rw₂ : ∀ (b : ℕ),
  Summable (α := ℂ) fun (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }) ↦
    (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z
Tactic: rw [Summable.tsum_prod' ?h₁ fun b ↦ ?h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Eq (α := ℂ) (∑' (b : ℕ) (c : (↑(gammaSet 1 b 0) : Type)), eisSummand (↑k : ℤ) (↑c : Fin 2 → ℤ) z)
    (∑' (b : ℕ) (c : { x : Fin 2 → ℤ // x ∈ gammaSet 1 1 0 }),
      (HPow.hPow (α := ℂ) (↑(b, c).1 : ℂ) k)⁻¹ * eisSummand (↑k : ℤ) (↑(b, c).2 : Fin 2 → ℤ) z)
have refine : ∀ (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: refine tsum_congr fun b ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
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)
have inl : 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: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
b : ℕ
inl :
  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)
⊢ 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)
have inr : ∀ (hb : b ≠ 0),
  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: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
b : ℕ
hb : b ≠ 0
⊢ 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)
have this : NeZero b
Tactic: have : NeZero b := ⟨hb⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ 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 : ℕ) : ℤ)
have 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 : ℕ)
Tactic: have HE1 := tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow hk hk2 z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
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 : ℕ)
⊢ 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 : ℕ) : ℤ)
have HE2 : ∑' (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