awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ @SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (eisensteinSeries a k)
      z =
    eisensteinSeries
      (a ᵥ*
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))
      k z
have h : (∑' (x : (↑(gammaSet N 1 a) : Type)), eisSummand k ((↑x : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) z) *
    denom
        ((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑z : ℂ) ^
      k =
  (∑' (x :
      (↑(gammaSet N 1
            (a ᵥ*
              (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                Matrix (Fin 2) (Fin 2) (ZMod N)))) :
        Type)),
      eisSummand k (↑x : Fin 2 → ℤ) z) *
    denom
        ((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
        (↑z : ℂ) ^
      k
Tactic: simp_rw [SL_slash_apply, zpow_neg,
    mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| denom_ne_zero _ z),
    eisensteinSeries, eisSummand_SL2_apply, tsum_mul_left, mul_comm (_ ^ k)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ (∑' (x : (↑(gammaSet N 1 a) : Type)), eisSummand k ((↑x : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) z) *
      denom
          ((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑z : ℂ) ^
        k =
    (∑' (x :
        (↑(gammaSet N 1
              (a ᵥ*
                (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                  Matrix (Fin 2) (Fin 2) (ZMod N)))) :
          Type)),
        eisSummand k (↑x : Fin 2 → ℤ) z) *
      denom
          ((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑z : ℂ) ^
        k
have h : Eq (α := ℂ) (∑' (x : (↑(gammaSet N 1 a) : Type)), eisSummand k ((↑x : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) z)
  (∑' (x :
    (↑(gammaSet N 1
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N)))) :
      Type)),
    eisSummand k (↑x : Fin 2 → ℤ) z)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
k : ℤ
A : GL (Fin 2) ℝ
hA : Membership.mem (γ := outParam (Subgroup (GL (Fin 2) ℝ))) (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) A
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (eisensteinSeries a k) =
    eisensteinSeries a k
have obtain : ∀ (A : SL(2, ℤ)) (hA : A ∈ Γ(N)),
  @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) A : GL (Fin 2) ℝ) (eisensteinSeries a k) =
    eisensteinSeries a k
Tactic: obtain ⟨A, (hA : A ∈ Γ(N)), rfl⟩ := hA
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
m : ℤ
z : ℍ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ eisSummand 2 ![m, n] z
have apply : ∀ (b : ℤ), (HPow.hPow (β := ℤ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)⁻¹ = eisSummand 2 ![m, b] z
Tactic: apply (linear_right_summable z m (k := 2) (by grind)).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
z : ℍ
n : ℤ
⊢ Eq (α := ℂ) ((fun (x : ℤ) ↦ e2Summand x z) (-n)) ((fun (x : ℤ) ↦ e2Summand x z) n)
have simp : Eq (α := ℂ) (∑' (d : ℤ), eisSummand 2 ![-n, -d] z) (∑' (n_1 : ℤ), eisSummand 2 ![n, n_1] z)
Tactic: simp only [e2Summand, ← tsum_comp_neg (fun a ↦ eisSummand 2 ![-n, a] z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
z : ℍ
n : ℤ
⊢ Eq (α := ℂ) (∑' (d : ℤ), eisSummand 2 ![-n, -d] z) (∑' (n_1 : ℤ), eisSummand 2 ![n, n_1] z)
have apply : ∀ (b : ℤ), eisSummand 2 ![-n, -b] z = eisSummand 2 ![n, b] z
Tactic: apply tsum_congr (fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
z : ℍ
n b : ℤ
⊢ eisSummand 2 ![-n, -b] z = eisSummand 2 ![n, b] z
have simp : HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)) + -(↑b : ℂ)) 2 = HPow.hPow (β := ℤ) ((↑n : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2
Tactic: simp only [eisSummand, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, Int.cast_neg, neg_mul, inv_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
⊢ D2 1 = 0
have h : ∀ (z : ℍ), D2 1 z = 0 z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (hypothesis)
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ (↑((↑(A * B) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B))
        (↑z : ℂ) =
    HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑(↑B : Matrix (Fin 2) (Fin 2) ℤ).det : ℂ) +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        denom
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) B) :
              GL (Fin 2) ℝ))
          (↑z : ℂ)
have h0 : ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
  ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 0 1 =
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ∧
    ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0 =
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ∧
      ((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 1 =
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1 +
          (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1
Tactic: have h0 := Matrix.two_mul_expl A.1 B.1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
A B : SL(2, ℤ)
⊢ D2 (A * B) = @SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 B
have h : ∀ (z : ℍ), D2 (A * B) z = (@SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 B) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ D2 (A * B) z = (@SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 B) z
have h : (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) /
    denom
      (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
      (↑z : ℂ) =
  (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
          (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
            ℂ) *
      (HPow.hPow (β := ℤ) (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ))
          2)⁻¹ +
    (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
      denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)
Tactic: simp only [D2, mul_assoc, coe_mul, map_mul, ← mul_div, SL_slash_def,
    ModularGroup.sl_moeb, Int.reduceNeg, zpow_neg, Pi.add_apply, ← mul_add, mul_eq_mul_left_iff,
    I_ne_zero, or_false, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (hypothesis)
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) /
      denom
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
        (↑z : ℂ) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
          denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
              ℂ) *
        (HPow.hPow (β := ℤ)
            (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) 2)⁻¹ +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)
have hd : (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
      denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) -
    (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
      denom
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
        (↑z : ℂ) =
  (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
Tactic: have hd : (A.1 * B.1) 1 0 * denom (φ B) z - B 1 0 * denom (φ A * φ B) z = A 1 0 := by
    simpa [sub_eq_iff_eq_add] using denom_aux A B z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (hypothesis)
Goal:
A B : SL(2, ℤ)
z : ℍ
hd :
  (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) *
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) -
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        denom
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
          (↑z : ℂ) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
⊢ (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) /
      denom
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A) : GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ))
        (↑z : ℂ) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
          denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
              ℂ) *
        (HPow.hPow (β := ℤ)
            (denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) 2)⁻¹ +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) /
        denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)
have this : denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
    (num ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ) /
      denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B)) (↑z : ℂ)) =
  denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) (↑(B • z) : ℂ)
Tactic: have : denom A (num B z / denom B z) = denom A ↑(B • z) := by
    simp [specialLinearGroup_apply, denom, num]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs (goal)
Goal:
⊢ D2 ModularGroup.T = 0
have h : ∀ (z : ℍ), D2 ModularGroup.T z = 0 z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable (goal)
Goal:
⊢ MDiff E2
have rw : DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
Tactic: rw [UpperHalfPlane.mdifferentiable_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable (hypothesis)
Goal:
⊢ DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have hη : DifferentiableOn ℂ η upperHalfPlaneSet
Tactic: have hη : DifferentiableOn ℂ η _ := fun z hz ↦
    (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).differentiableWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable (hypothesis)
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
Tactic: have hlog : DifferentiableOn ℂ (logDeriv η) _ :=
    (hη.deriv isOpen_upperHalfPlaneSet).div hη (fun _ hz ↦ eta_ne_zero hz)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable (goal)
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have refine : ∀ (z : ℂ) (hz : z ∈ upperHalfPlaneSet), (E2 ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑π : ℂ) * I / 12)⁻¹ * logDeriv η z
Tactic: refine (hlog.const_mul (π * I / 12)⁻¹).congr (fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable (goal)
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ (E2 ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑π : ℂ) * I / 12)⁻¹ * logDeriv η z
have simp : E2 { coe := z, coe_im_pos := hz : ℍ } =
  12 / ((↑π : ℂ) * I) * ((↑π : ℂ) * I / 12 * E2 { coe := z, coe_im_pos := hz : ℍ })
Tactic: simp [ofComplex_apply_of_im_pos hz, logDeriv_eta_eq_E2 ⟨z, hz⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ ∑ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), e2Summand m z =
    2 * riemannZeta 2 +
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
have rw : HMul.hMul (α := ℂ) (↑2 : ℂ) (∑ k ∈ range N, e2Summand (↑(k + 1) : ℤ) z) + HSMul.hSMul (α := ℕ) 2 (2 * riemannZeta 2) -
    2 * riemannZeta 2 =
  2 * riemannZeta 2 +
    ∑ m ∈ range N,
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
Tactic: rw [sum_Icc_of_even_eq_range (e2Summand_even z), Finset.sum_range_succ', smul_add,
    nsmul_eq_mul, Nat.cast_zero, e2Summand_zero_eq_two_riemannZeta_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ HMul.hMul (α := ℂ) (↑2 : ℂ) (∑ k ∈ range N, e2Summand (↑(k + 1) : ℤ) z) + HSMul.hSMul (α := ℕ) 2 (2 * riemannZeta 2) -
      2 * riemannZeta 2 =
    2 * riemannZeta 2 +
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
have ring_nf : HMul.hMul (α := ℂ) (∑ x ∈ range N, e2Summand (↑(1 + x) : ℤ) z) 2 + riemannZeta 2 * 2 =
  riemannZeta 2 * 2 +
    ∑ x ∈ range N,
      -((HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            ∑' (n : ℕ+),
              (↑(↑n : ℕ) : ℂ) * cexp ((↑π : ℂ) * I * (↑z : ℂ) * 2) ^ (x * (↑n : ℕ)) *
                cexp ((↑π : ℂ) * I * (↑z : ℂ) * 2) ^ (↑n : ℕ)) *
          8)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ HMul.hMul (α := ℂ) (∑ x ∈ range N, e2Summand (↑(1 + x) : ℤ) z) 2 + riemannZeta 2 * 2 =
    riemannZeta 2 * 2 +
      ∑ x ∈ range N,
        -((HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
              ∑' (n : ℕ+),
                (↑(↑n : ℕ) : ℂ) * cexp ((↑π : ℂ) * I * (↑z : ℂ) * 2) ^ (x * (↑n : ℕ)) *
                  cexp ((↑π : ℂ) * I * (↑z : ℂ) * 2) ^ (↑n : ℕ)) *
            8)
have simp : 2 * riemannZeta 2 +
    ∑ i ∈ range N,
      HMul.hMul (α := ℂ) 2
        (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2)⁻¹) =
  2 * riemannZeta 2 +
    ∑ x ∈ range N,
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            ∑' (n : ℕ+),
              cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
                (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (x * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
Tactic: simp only [e2Summand, eisSummand, add_comm, Nat.cast_add, Nat.cast_one, Fin.isValue,
    Matrix.cons_val_zero, Int.cast_add, Int.cast_natCast, Int.cast_one, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, mul_comm, mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ 2 * riemannZeta 2 +
      ∑ i ∈ range N,
        HMul.hMul (α := ℂ) 2
          (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2)⁻¹) =
    2 * riemannZeta 2 +
      ∑ x ∈ range N,
        -(8 *
            (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
              ∑' (n : ℕ+),
                cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
                  (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (x * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
have e_a : ∀ (a : ℕ),
  HMul.hMul (α := ℂ) 2 (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+),
            cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
              (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (a * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
Tactic: congr with a
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
N a : ℕ
⊢ HMul.hMul (α := ℂ) 2 (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+),
            cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
              (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (a * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
have H2 : ∑' (n : ℤ),
    1 /
      ((↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ) + (↑n : ℂ)) ^
        HAdd.hAdd (α := ℕ) 1 1 =
  (-2 * (↑π : ℂ) * I) ^ HAdd.hAdd (α := ℕ) 1 1 / (↑1! : ℂ) *
    ∑' (n : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 *
        cexp (2 * (↑π : ℂ) * I * (↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^
          (↑n : ℕ)
Tactic: have H2 := qExpansion_identity_pnat (k := 1) (by grind)
    ⟨(a + 1) * z, by simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ),
      1 /
        ((↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) + (↑n : ℂ)) ^
          HAdd.hAdd (α := ℕ) 1 1 =
    (-2 * (↑π : ℂ) * I) ^ HAdd.hAdd (α := ℕ) 1 1 / (↑1! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 *
          cexp (2 * (↑π : ℂ) * I * (↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
            (↑n : ℕ)
⊢ HMul.hMul (α := ℂ) 2 (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+),
            cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
              (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (a * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
have H2₁ : ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
  HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
    ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
Tactic: simp only [add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
    Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one] at H2
Cleared hypotheses: H2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
⊢ HMul.hMul (α := ℂ) 2 (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+),
            cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
              (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (a * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))
have e_a : Eq (α := ℂ)
  (∑' (x : ℕ+),
    2 *
      (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
        (cexp ((↑x : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑x : ℕ) : ℂ))))
  (∑' (b : ℕ+),
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
            (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ))))))
Tactic: simp_rw [zpow_ofNat, H2, ← tsum_mul_left, ← tsum_neg, ← exp_nsmul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
⊢ Eq (α := ℂ)
    (∑' (x : ℕ+),
      2 *
        (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
          (cexp ((↑x : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑x : ℕ) : ℂ))))
    (∑' (b : ℕ+),
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
              (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ))))))
have e_a : ∀ (b : ℕ+),
  2 *
      (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
        (cexp ((↑b : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑b : ℕ) : ℂ))) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
            (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ)))))
Tactic: refine tsum_congr fun b ↦ ?_