awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have simp_rw₃ : Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a) ((↑v : Fin 2 → ℤ) ᵥ* (↑(γ * γ⁻¹) : Matrix (Fin 2) (Fin 2) ℤ))
    sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have simp_rw₄ : Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a) ((↑v : Fin 2 → ℤ) ᵥ* (↑1 : Matrix (Fin 2) (Fin 2) ℤ)) sorry = v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have simp_rw₅ : Subtype.mk (p := fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet N r a) ((↑v : Fin 2 → ℤ) ᵥ* 1) sorry = v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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)
⊢ (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
have 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) ℤ)) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have 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) ℤ))) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have 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) ℤ)) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have 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) ℤ)) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ (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
have 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) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ 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
have 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)
Tactic: simp only [eisSummand, vecMul, vec2_dotProduct, denom, UpperHalfPlane.specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * (↑z : ℂ) + d ≠ 0
⊢ (↑z : ℂ) * c + d ≠ 0
have h : (↑z : ℂ) * c + d = c * (↑z : ℂ) + d
Tactic: convert! hc using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
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)
have hc₁ : (↑z : ℂ) * c + d ≠ 0
Tactic: replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : (↑z : ℂ) * c + 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)
have 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)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : (↑z : ℂ) * c + d ≠ 0
⊢ ((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)
have 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)⁻¹
Tactic: simp [div_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ ((↑(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)
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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
⊢ @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
have 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
Tactic: ext1 z