awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∀ (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 : ℕ)

Tactic:
have H (b : ℕ+) := qExpansion_identity_pnat (k := k - 1) (by grind) ⟨b * z, by simpa using z.2⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), 1 / ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑n : ℂ)) ^ (k - 1 + 1) =
      (-2 * (↑π : ℂ) * I) ^ (k - 1 + 1) / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp (2 * (↑π : ℂ) * I * ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ))) ^ (↑n : ℕ)
⊢ k - 1 + 1 = k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
⊢ ∀ (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

Premises used: one_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
⊢ ∀ (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

Premises used: neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
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 : ℕ))
⊢ ∑' (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 [nsmul_eq_mul, mul_assoc]

Premises used: mul_assoc, nsmul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℂ)
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 : ℕ)
⊢ ∑' (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:
congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
⊢ 2 ≤ k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 = 2 * riemannZeta (↑k : ℂ)

Tactic:
simp [eisSummand, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (by grind) hk2]

Premises used: two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, EisensteinSeries.eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ)
this :
  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 : ℕ)))
⊢ ∑' (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:
simp [eisSummand, H, tsum_mul_left,
        ← tsum_prod_pow_eq_tsum_sigma (k - 1) (norm_exp_two_pi_I_lt_one z), this]

Premises used: HSub.hSub, UpperHalfPlane.norm_exp_two_pi_I_lt_one, tsum_mul_left, tsum_prod_pow_eq_tsum_sigma, EisensteinSeries.eisSummand, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 :
  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 : ℕ)))
⊢ ∑' (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:
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]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 :
  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 : ℂ))))
⊢ 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:
simp_rw [← Complex.exp_nat_mul]

Premises used: Complex.exp_nat_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 : ℕ+
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 : ℂ)))
⊢ HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) *
      cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)))) =
    HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp ((↑((↑m : ℕ) * (↑n : ℕ)) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ)))

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 (HMul.hMul (α := ℂ) (↑(↑m : ℕ) : ℂ) (↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ)))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)))))
    (∑' (m : ℕ+) (n : ℕ+),
      HPow.hPow (α := ℂ) (↑(↑n : ℕ) : ℂ) (k - 1) * cexp ((↑((↑m : ℕ) * (↑n : ℕ)) : ℂ) * (2 * (↑π : ℂ) * I * (↑z : ℂ))))

Tactic:
exact tsum_congr₂ (fun m n ↦ by push_cast; ring_nf)

Premises used: tsum_congr₂
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℤ
z : ℍ
n : ℕ
v : (↑(gammaSet 1 n 0) : Type)
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)
⊢ ((↑((↑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)

Tactic:
nth_rw 1 2 [gammaSet_eq_gcd_mul_divIntMap v.2]

Premises used: Subtype.property, EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℤ
z : ℍ
n : ℕ
v : (↑(gammaSet 1 n 0) : Type)
⊢ ((↑((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:
simp [← mul_inv, ← mul_zpow, mul_add, mul_assoc]

Premises used: mul_inv, mul_assoc, mul_zpow, mul_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ 1 < k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ 1 < k

Tactic:
have hk1 : 1 < k := by grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
⊢ LE.le (α := ℤ) 3 (↑k : ℤ)

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

Tactic:
simp_rw [← gammaSetDivGcdSigmaEquiv.symm.tsum_eq, gammaSetDivGcdSigmaEquiv_symm_eq]

Premises used: EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq, Equiv.tsum_eq, Equiv.symm, EisensteinSeries.gammaSetDivGcdSigmaEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖

Tactic:
simp [hk1]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
rw₁ :
  Summable (α := ℂ) fun (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)) ↦
    eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : 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

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

Premises used: Summable.subtype, Summable.tsum_sigma, tsum_mul_tsum_of_summable_norm, EisensteinSeries.summable_norm_eisSummand, eisensteinSeries, zeta_nat_eq_tsum_of_gt_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ ∀ (b : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)),
    ((fun (x : Fin 2 → ℤ) ↦ eisSummand (↑k : ℤ) x z) ∘
          (⇑gammaSetDivGcdSigmaEquiv.symm : (a : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)) → Fin 2 → ℤ))
        b =
      eisSummand (↑k : ℤ) (↑(b.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Summable (α := ℂ) fun (c : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)) ↦
    eisSummand (↑k : ℤ) (↑(c.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ) z

Tactic:
case hsumm =>
    exact gammaSetDivGcdSigmaEquiv.symm.summable_iff.mpr (summable_norm_eisSummand hk2 z).of_norm
      |>.congr <| by simp

Premises used: Iff.mpr, Summable.of_norm, EisensteinSeries.summable_norm_eisSummand, Equiv.summable_iff, Summable.congr, Equiv.symm, EisensteinSeries.gammaSetDivGcdSigmaEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
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)
⊢ 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:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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
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
⊢ 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:
rw [Summable.tsum_prod' ?h₁ fun b ↦ ?h₂]

Premises used: Summable.tsum_prod'
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((fun (n : ℕ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹) x)

Tactic:
simp [hk1]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ 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:
exact summable_mul_of_summable_norm (f := fun (n : ℕ) ↦ ((n : ℂ) ^ k)⁻¹)
      (g := fun (v : gammaSet 1 1 0) ↦ eisSummand k v z) (by simp [hk1])
      ((summable_norm_eisSummand hk2 z).subtype _)

Premises used: summable_mul_of_summable_norm, Summable.subtype, EisensteinSeries.summable_norm_eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
⊢ 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:
case h₁ =>
    exact summable_mul_of_summable_norm (f := fun (n : ℕ) ↦ ((n : ℂ) ^ k)⁻¹)
      (g := fun (v : gammaSet 1 1 0) ↦ eisSummand k v z) (by simp [hk1])
      ((summable_norm_eisSummand hk2 z).subtype _)

Premises used: summable_mul_of_summable_norm, Summable.subtype, EisensteinSeries.summable_norm_eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
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:
simpa using ((summable_norm_eisSummand hk2 z).subtype _).of_norm.mul_left (a := ((b : ℂ) ^ k)⁻¹)

Premises used: Summable.of_norm, Summable.subtype, EisensteinSeries.summable_norm_eisSummand, Nat.cast, Summable.mul_left, Inv.inv, HPow.hPow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
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:
case h₂ =>
    simpa using ((summable_norm_eisSummand hk2 z).subtype _).of_norm.mul_left (a := ((b : ℂ) ^ k)⁻¹)

Premises used: Summable.of_norm, Summable.subtype, EisensteinSeries.summable_norm_eisSummand, Nat.cast, Summable.mul_left, Inv.inv, HPow.hPow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)

Tactic:
tsum_congr fun b ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : LE.le (α := ℤ) 3 (↑k : ℤ)
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)
⊢ 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:
refine tsum_congr fun b ↦ ?_

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

Premises used: eq_or_ne, OfNat.ofNat, rfl