awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
γ : SL(2, ℤ)
v : (↑(gammaSet N r a) : Type)
simp_rw simp_rw₁ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a)
      ((↑v : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ =
    v
simp_rw₂ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a)
      ((↑v : Fin 2 → ℤ) ᵥ* ((↑γ : Matrix (Fin 2) (Fin 2) ℤ) * (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ))) ⋯ =
    v
simp_rw₃ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a)
      ((↑v : Fin 2 → ℤ) ᵥ* (↑(γ * γ⁻¹) : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ =
    v
simp_rw₄ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a) ((↑v : Fin 2 → ℤ) ᵥ* (↑1 : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ = v
simp_rw₅ : Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a) ((↑v : Fin 2 → ℤ) ᵥ* 1) ⋯ = v
⊢ (fun
          (v :
            (↑(gammaSet N r
                  (a ᵥ*
                    (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                      Matrix (Fin 2) (Fin 2) (ZMod N)))) :
              Type)) ↦
        Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a)
          ((↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯)
      ((fun (v : (↑(gammaSet N r a) : Type)) ↦
          Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
            x ∈
              gammaSet N r
                (a ᵥ*
                  (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                    Matrix (Fin 2) (Fin 2) (ZMod N))))
            ((↑v : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯)
        v) =
    v

Tactic:
simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]

Premises used: Matrix.SpecialLinearGroup.coe_one, Matrix.vecMul_vecMul, mul_inv_cancel, Matrix.SpecialLinearGroup.coe_mul, Matrix.vecMul_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
γ : SL(2, ℤ)
v :
  (↑(gammaSet N r
        (a ᵥ*
          (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
            Matrix (Fin 2) (Fin 2) (ZMod N)))) :
    Type)
simp_rw simp_rw₁ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
      x ∈
        gammaSet N r
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N))))
      ((↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ =
    v
simp_rw₂ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
      x ∈
        gammaSet N r
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N))))
      ((↑v : Fin 2 → ℤ) ᵥ* ((↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) * (↑γ : Matrix (Fin 2) (Fin 2) ℤ))) ⋯ =
    v
simp_rw₃ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
      x ∈
        gammaSet N r
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N))))
      ((↑v : Fin 2 → ℤ) ᵥ* (↑(γ⁻¹ * γ) : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ =
    v
simp_rw₄ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
      x ∈
        gammaSet N r
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N))))
      ((↑v : Fin 2 → ℤ) ᵥ* (↑1 : Matrix (Fin 2) (Fin 2) ℤ)) ⋯ =
    v
simp_rw₅ :
  Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
      x ∈
        gammaSet N r
          (a ᵥ*
            (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
              Matrix (Fin 2) (Fin 2) (ZMod N))))
      ((↑v : Fin 2 → ℤ) ᵥ* 1) ⋯ =
    v
⊢ (fun (v : (↑(gammaSet N r a) : Type)) ↦
        Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦
          x ∈
            gammaSet N r
              (a ᵥ*
                (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                  Matrix (Fin 2) (Fin 2) (ZMod N))))
          ((↑v : Fin 2 → ℤ) ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯)
      ((fun
            (v :
              (↑(gammaSet N r
                    (a ᵥ*
                      (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
                        Matrix (Fin 2) (Fin 2) (ZMod N)))) :
                Type)) ↦
          Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a)
            ((↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ)) ⋯)
        v) =
    v

Tactic:
simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]

Premises used: inv_mul_cancel, Matrix.SpecialLinearGroup.coe_one, Matrix.vecMul_vecMul, Matrix.SpecialLinearGroup.coe_mul, Matrix.vecMul_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
simp :
  ((↑(i 0) : ℂ) *
          (((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
            ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ))) +
        (↑(i 1) : ℂ)) ^
      (-k) =
    ((↑((↑((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 0) :
              ℂ) *
            (↑z : ℂ) +
          (↑((↑((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                      ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) :
                  Matrix (Fin 2) (Fin 2) ℝ)
                1 1) :
            ℂ)) ^
        k *
      ((↑(i 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 + i 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) +
          (↑(i 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 + i 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^
        (-k)
⊢ eisSummand k i (A • z) =
    denom
          ((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
          (↑z : ℂ) ^
        k *
      eisSummand k (i ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) z

Tactic:
simp only [eisSummand, vecMul, vec2_dotProduct, denom, UpperHalfPlane.specialLinearGroup_apply]

Premises used: UpperHalfPlane.specialLinearGroup_apply, Matrix.vecMul, UpperHalfPlane.denom, EisensteinSeries.eisSummand, Matrix.vec2_dotProduct
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * (↑z : ℂ) + d ≠ 0
⊢ c * (↑z : ℂ) + d ≠ 0

Tactic:
hc
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * (↑z : ℂ) + d ≠ 0
h : (↑z : ℂ) * c + d = c * (↑z : ℂ) + d
⊢ (↑z : ℂ) * c + d ≠ 0

Tactic:
convert! hc using 1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * (↑z : ℂ) + d ≠ 0
⊢ (↑z : ℂ) * c + d = c * (↑z : ℂ) + d

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * (↑z : ℂ) + d ≠ 0
⊢ (↑z : ℂ) * c + d ≠ 0

Tactic:
replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : (↑z : ℂ) * c + d ≠ 0
field_simp :
  ((u * (a * (↑z : ℂ) + b) + ((↑z : ℂ) * c + d) * v) / ((↑z : ℂ) * c + d)) ^ (-k) =
    ((↑z : ℂ) * c + d) ^ k * ((↑z : ℂ) * (u * a + c * v) + (u * b + d * v)) ^ (-k)
⊢ (u * ((a * (↑z : ℂ) + b) / (c * (↑z : ℂ) + d)) + v) ^ (-k) =
    (c * (↑z : ℂ) + d) ^ k * ((u * a + v * c) * (↑z : ℂ) + (u * b + v * d)) ^ (-k)

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : (↑z : ℂ) * c + d ≠ 0
simp :
  ((↑z : ℂ) * c + d) ^ k / (u * (a * (↑z : ℂ) + b) + ((↑z : ℂ) * c + d) * v) ^ k =
    ((↑z : ℂ) * c + d) ^ k * (((↑z : ℂ) * (u * a + c * v) + (u * b + d * v)) ^ k)⁻¹
⊢ ((u * (a * (↑z : ℂ) + b) + ((↑z : ℂ) * c + d) * v) / ((↑z : ℂ) * c + d)) ^ (-k) =
    ((↑z : ℂ) * c + d) ^ k * ((↑z : ℂ) * (u * a + c * v) + (u * b + d * v)) ^ (-k)

Tactic:
simp [div_zpow]

Premises used: div_zpow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : (↑z : ℂ) * c + d ≠ 0
⊢ ((↑z : ℂ) * c + d) ^ k / (u * (a * (↑z : ℂ) + b) + ((↑z : ℂ) * c + d) * v) ^ k =
    ((↑z : ℂ) * c + d) ^ k * (((↑z : ℂ) * (u * a + c * v) + (u * b + d * v)) ^ k)⁻¹

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ ∀ (a b c d u v : ℂ) (hc : c * (↑z : ℂ) + d ≠ 0),
    (u * ((a * (↑z : ℂ) + b) / (c * (↑z : ℂ) + d)) + v) ^ (-k) =
      (c * (↑z : ℂ) + d) ^ k * ((u * a + v * c) * (↑z : ℂ) + (u * b + v * d)) ^ (-k)

Tactic:
have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : (u * ((a * z + b) / (c * z + d)) + v) ^ (-k) =
      (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) := by
    replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
    field_simp
    simp [div_zpow]
    ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ) (hc : c * (↑z : ℂ) + d ≠ 0),
    (u * ((a * (↑z : ℂ) + b) / (c * (↑z : ℂ) + d)) + v) ^ (-k) =
      (c * (↑z : ℂ) + d) ^ k * ((u * a + v * c) * (↑z : ℂ) + (u * b + v * d)) ^ (-k)
⊢ ((↑(i 0) : ℂ) *
          (((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
            ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ))) +
        (↑(i 1) : ℂ)) ^
      (-k) =
    ((↑((↑((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 0) :
              ℂ) *
            (↑z : ℂ) +
          (↑((↑((SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                      ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A)) :
                  Matrix (Fin 2) (Fin 2) ℝ)
                1 1) :
            ℂ)) ^
        k *
      ((↑(i 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 + i 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) +
          (↑(i 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 + i 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^
        (-k)

Tactic:
simpa using h (hc := denom_ne_zero A z) ..

Premises used: Real, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
h :
  ∀ (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
⊢ @SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (eisensteinSeries a k) =
    eisensteinSeries
      (a ᵥ*
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))
      k

Tactic:
ext1 z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
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
⊢ @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

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

Premises used: tsum_mul_left, HPow.hPow, zpow_neg, eisensteinSeries, mul_comm, mul_inv_eq_iff_eq_mul₀, zpow_ne_zero, ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
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)
⊢ (∑' (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:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ 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:
(gammaSetEquiv a γ).tsum_eq (eisSummand k · z)

Premises used: Multiset.sum, Multiset.foldr, EisensteinSeries.gammaSetEquiv, dotProduct, Matrix.vecMul, Equiv.tsum_eq, EisensteinSeries.eisSummand, Subtype.val, List.foldr, Finset.sum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ 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:
exact (gammaSetEquiv a γ).tsum_eq (eisSummand k · z)

Premises used: EisensteinSeries.gammaSetEquiv, Equiv.tsum_eq, EisensteinSeries.eisSummand, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
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
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
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (eisensteinSeries a k) =
    eisensteinSeries a k

Tactic:
obtain ⟨A, (hA : A ∈ Γ(N)), rfl⟩ := hA

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
k : ℤ
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:
simp [SpecialLinearGroup.mapGL, ← SL_slash, eisensteinSeries_slash_apply, Gamma_mem'.mp hA]

Premises used: CongruenceSubgroup.Gamma_mem', ModularForm.SL_slash, Iff.mp, Matrix.SpecialLinearGroup.mapGL, EisensteinSeries.eisensteinSeries_slash_apply
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
z : ℍ
⊢ (eisensteinSeriesSIF a k : (a : ℍ) → ℂ) z = eisensteinSeries a k z

Tactic:
rfl

Premises used: tsum, eisensteinSeries, rfl