awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
m : ℤ
z : ℍ
⊢ LE.le (α := ℤ) 2 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
m : ℤ
z : ℍ
apply : ∀ (b : ℤ), (HPow.hPow (β := ℤ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)⁻¹ = eisSummand 2 ![m, b] z
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ eisSummand 2 ![m, n] z

Tactic:
apply (linear_right_summable z m (k := 2) (by grind)).congr

Premises used: UpperHalfPlane.coe, EisensteinSeries.linear_right_summable, Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
m : ℤ
z : ℍ
⊢ ∀ (b : ℤ), (HPow.hPow (β := ℤ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)⁻¹ = eisSummand 2 ![m, b] z

Tactic:
simp [eisSummand]

Premises used: EisensteinSeries.eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ LE.le (α := ℕ) 2 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ Even (α := ℕ) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ e2Summand 0 z = 2 * riemannZeta 2

Tactic:
simpa [e2Summand, eisSummand] using
    (two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (k := 2) (by grind) (by simp)).symm

Premises used: two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, EisensteinSeries.e2Summand, EisensteinSeries.eisSummand, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
n : ℤ
simp : Eq (α := ℂ) (∑' (d : ℤ), eisSummand 2 ![-n, -d] z) (∑' (n_1 : ℤ), eisSummand 2 ![n, n_1] z)
⊢ Eq (α := ℂ) ((fun (x : ℤ) ↦ e2Summand x z) (-n)) ((fun (x : ℤ) ↦ e2Summand x z) n)

Tactic:
simp only [e2Summand, ← tsum_comp_neg (fun a ↦ eisSummand 2 ![-n, a] z)]

Premises used: tsum_comp_neg, EisensteinSeries.e2Summand, Matrix.vecEmpty, EisensteinSeries.eisSummand, OfNat.ofNat, Matrix.vecCons, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
n : ℤ
apply : ∀ (b : ℤ), eisSummand 2 ![-n, -b] z = eisSummand 2 ![n, b] z
⊢ Eq (α := ℂ) (∑' (d : ℤ), eisSummand 2 ![-n, -d] z) (∑' (n_1 : ℤ), eisSummand 2 ![n, n_1] z)

Tactic:
apply tsum_congr (fun b ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
n b : ℤ
simp : HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)) + -(↑b : ℂ)) 2 = HPow.hPow (β := ℤ) ((↑n : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2
⊢ eisSummand 2 ![-n, -b] z = eisSummand 2 ![n, b] z

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]

Premises used: Int.cast_neg, Int.reduceNeg, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val_fin_one, inv_inj, Fin.isValue, zpow_neg, EisensteinSeries.eisSummand, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
n b : ℤ
⊢ HPow.hPow (β := ℕ) (-((↑n : ℂ) * (↑z : ℂ)) + -(↑b : ℂ)) 2 = HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
h : ∀ (z : ℍ), D2 1 z = 0 z
⊢ D2 1 = 0

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ D2 1 z = 0 z

Tactic:
simp [D2]

Premises used: EisensteinSeries.D2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ ((↑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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
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
⊢ (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
        HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
      ((↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) =
    (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        (HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ) -
          HMul.hMul (α := ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ)
            (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) +
      (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) *
        ((HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ℂ) +
              HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
                (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)) *
            (↑z : ℂ) +
          (HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)
              (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℂ) +
            HMul.hMul (α := ℂ) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)
              (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
h :
  ∀ (z : ℍ), D2 (A * B) z = (@SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 B) z
⊢ D2 (A * B) = @SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 B

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
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 : ℂ)
⊢ D2 (A * B) z = (@SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 B (D2 A) + D2 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]

Premises used: mul_div, OfNat.ofNat_ne_zero, ModularGroup.sl_moeb, Int.reduceNeg, mul_assoc, mul_eq_mul_left_iff, Complex.I_ne_zero, Pi.add_apply, map_mul, Complex.ofReal_eq_zero, ModularForm.SL_slash_def, zpow_neg, mul_add, or_false, EisensteinSeries.D2, Matrix.SpecialLinearGroup.coe_mul, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ (↑(((↑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:
simpa [sub_eq_iff_eq_add] using denom_aux A B z

Premises used: _private.0.EisensteinSeries.denom_aux, sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A B : SL(2, ℤ)
z : ℍ
⊢ (↑(((↑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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
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) : ℂ)
⊢ 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:
simp [specialLinearGroup_apply, denom, num]

Premises used: UpperHalfPlane.specialLinearGroup_apply, UpperHalfPlane.denom, UpperHalfPlane.num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
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) : ℂ)
⊢ 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]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
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) : ℂ)
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) : ℂ)
a b c d f e : ℂ
he : e ≠ 0
⊢ a / b = c / d * (HPow.hPow (β := ℤ) e 2)⁻¹ + f / e ↔ a * HPow.hPow (β := ℕ) e 2 / b = c / d + e * f

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
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) : ℂ)
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) : ℂ)
⊢ (↑(((↑A : Matrix (Fin 2) (Fin 2) ℤ) * (↑B : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ℂ) =
    (↑(((↑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, ℝ)) A))
            (↑(HSMul.hSMul (α := GL (Fin 2) ℝ)
                  ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((φ : (a : SL(2, ℤ)) → SL(2, ℝ)) B) : GL (Fin 2) ℝ) z) :
              ℂ) *
          (↑((↑B : 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) :
            ℂ) *
        (↑((↑B : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
A : SL(2, ℤ)
⊢ @SlashAction.map ℤ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 A⁻¹ (D2 A) = -D2 A⁻¹

Tactic:
simpa [eq_neg_iff_add_eq_zero] using (D2_mul A A⁻¹).symm

Premises used: Inv.inv, eq_neg_iff_add_eq_zero, Eq.symm, EisensteinSeries.D2_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
h : ∀ (z : ℍ), D2 ModularGroup.T z = 0 z
⊢ D2 ModularGroup.T = 0

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ D2 ModularGroup.T z = 0 z

Tactic:
simp [D2, ModularGroup.T]

Premises used: ModularGroup.T, EisensteinSeries.D2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
Goal:
z : ℍ
⊢ D2 ModularGroup.S z = 2 * (↑π : ℂ) * I / (↑z : ℂ)

Tactic:
simp [D2, ModularGroup.S, ModularGroup.denom_apply]

Premises used: ModularGroup.denom_apply, ModularGroup.S, EisensteinSeries.D2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
rw : DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
⊢ MDiff E2

Tactic:
rw [UpperHalfPlane.mdifferentiable_iff]

Premises used: UpperHalfPlane.mdifferentiable_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

Tactic:
have hη : DifferentiableOn ℂ η _ := fun z hz ↦
    (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).differentiableWithinAt
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
⊢ DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet

Tactic:
have hlog : DifferentiableOn ℂ (logDeriv η) _ :=
    (hη.deriv isOpen_upperHalfPlaneSet).div hη (fun _ hz ↦ eta_ne_zero hz)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
(hlog.const_mul (π * I / 12)⁻¹).congr (fun z hz ↦ ?_)

Premises used: Real.pi, DifferentiableOn.congr, HMul.hMul, HDiv.hDiv, Complex.ofReal, Inv.inv, DifferentiableOn.const_mul, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
refine : ∀ (z : ℂ) (hz : z ∈ upperHalfPlaneSet), (E2 ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑π : ℂ) * I / 12)⁻¹ * logDeriv η z
⊢ DifferentiableOn ℂ (E2 ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
refine (hlog.const_mul (π * I / 12)⁻¹).congr (fun z hz ↦ ?_)

Premises used: Real.pi, DifferentiableOn.congr, HMul.hMul, HDiv.hDiv, Complex.ofReal, Inv.inv, DifferentiableOn.const_mul, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
simp :
  E2 { coe := z, coe_im_pos := hz : ℍ } =
    12 / ((↑π : ℂ) * I) * ((↑π : ℂ) * I / 12 * E2 { coe := z, coe_im_pos := hz : ℍ })
⊢ (E2 ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑π : ℂ) * I / 12)⁻¹ * logDeriv η z

Tactic:
simp [ofComplex_apply_of_im_pos hz, logDeriv_eta_eq_E2 ⟨z, hz⟩]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, UpperHalfPlane.mk, ModularForm.logDeriv_eta_eq_E2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable
Goal:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ E2 { coe := z, coe_im_pos := hz : ℍ } =
    12 / ((↑π : ℂ) * I) * ((↑π : ℂ) * I / 12 * E2 { coe := z, coe_im_pos := hz : ℍ })

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
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 : ℕ))
⊢ ∑ 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 : ℕ))

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]

Premises used: EisensteinSeries.e2Summand_even, EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two, Finset.sum_Icc_of_even_eq_range, nsmul_eq_mul, Nat.cast_zero, Finset.sum_range_succ', smul_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
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)
⊢ 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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
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 : ℕ) : ℂ))))
⊢ 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:
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]

Premises used: Finset.mul_sum, Int.cast_natCast, Int.reduceNeg, Matrix.cons_val_one, Matrix.cons_val_zero, Int.cast_add, Matrix.cons_val_fin_one, add_comm, EisensteinSeries.e2Summand, Nat.cast_add, Fin.isValue, zpow_neg, EisensteinSeries.eisSummand, mul_comm, Nat.cast_one, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
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 : ℕ) : ℂ))))
⊢ 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:
congr with a