awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
rw :
  IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 1)
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑r : Fin 2 → ℤ) 0) (HDiv.hDiv (β := Fin 2 → ℤ) v (↑r : Fin 2 → ℤ) 1)

Tactic:
rw [← hv]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
hpq : @gcd _ CommSemiring.toCommMonoidWithZero _ (v 0) (v 1) ≠ 0
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 1)

Tactic:
apply isCoprime_div_gcd_div_gcd_of_gcd_ne_zero

Premises used: isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ r ≠ 0

Tactic:
have := NeZero.ne r
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
this : r ≠ 0
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (v 0) (v 1) ≠ 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
a : ℤ
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ finGcdMap (a • v) = a.natAbs * r

Tactic:
simp [finGcdMap, Int.gcd_mul_left, hv]

Premises used: EisensteinSeries.finGcdMap, Int.gcd_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
v : Fin 2 → ℤ
rw : (v 0).gcd (v 1) = 1 ↔ IsCoprime (v 0) (v 1)
rw₁ rw₂ : (v 0).gcd (v 1) = 1 ↔ (v 0).gcd (v 1) = 1
⊢ v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

Tactic:
rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]

Premises used: Int.isCoprime_iff_gcd_eq_one, EisensteinSeries.gammaSet_one_mem_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
i : Fin 2
0 : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
1 : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (↑r : ℤ) ∣ v i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

Premises used: And.right, Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

Premises used: And.right, Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
⊢ BijOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro, Set.BijOn
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
refine_1 : MapsTo (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
refine_2 : InjOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0)
refine_3 : SurjOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
⊢ BijOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
refine_1 :
  IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 1)
⊢ divIntMap (↑r : ℤ) x ∈ gammaSet 1 1 0

Tactic:
simp only [divIntMap, mem_gammaSet_one] at *

Premises used: EisensteinSeries.divIntMap, EisensteinSeries.mem_gammaSet_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 1)

Tactic:
finGcdMap_div _ hx.2

Premises used: EisensteinSeries.finGcdMap_div, And.right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 1)

Tactic:
exact finGcdMap_div _ hx.2

Premises used: EisensteinSeries.finGcdMap_div, And.right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hv2 : divIntMap (↑r : ℤ) x = divIntMap (↑r : ℤ) v
refine_2 : ∀ (i : Fin 2), x i = v i
⊢ x = v

Tactic:
ext i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hv2 : divIntMap (↑r : ℤ) x = divIntMap (↑r : ℤ) v
i : Fin 2
⊢ x i = v i

Tactic:
(Int.ediv_left_inj (gammaSet_div_gcd hx i) (gammaSet_div_gcd hv i)).mp
      (congr_fun hv2 i)

Premises used: Int.ediv_left_inj, Iff.mp, congr_fun, EisensteinSeries.gammaSet_div_gcd
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hv2 : divIntMap (↑r : ℤ) x = divIntMap (↑r : ℤ) v
i : Fin 2
⊢ x i = v i

Tactic:
exact (Int.ediv_left_inj (gammaSet_div_gcd hx i) (gammaSet_div_gcd hv i)).mp
      (congr_fun hv2 i)

Premises used: Int.ediv_left_inj, Iff.mp, congr_fun, EisensteinSeries.gammaSet_div_gcd
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
h : r • x ∈ gammaSet 1 r 0 ∧ divIntMap (↑r : ℤ) (r • x) = x
⊢ x ∈ divIntMap (↑r : ℤ) '' gammaSet 1 r 0

Tactic:
use r • x
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
h : (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0
h₁ : (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x
⊢ (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0 ∧ (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ (x 0).gcd (x 1) = 1

Tactic:
rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx

Premises used: Int.isCoprime_iff_gcd_eq_one, EisensteinSeries.mem_gammaSet_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : (x 0).gcd (x 1) = 1
⊢ (HMul.hMul (α := Fin 2 → ℤ) (↑r : Fin 2 → ℤ) x 0).gcd (HMul.hMul (α := Fin 2 → ℤ) (↑r : Fin 2 → ℤ) x 1) = r

Tactic:
simp [Int.gcd_mul_left, hx]

Premises used: Int.gcd_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : (x 0).gcd (x 1) = 1
⊢ (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0

Tactic:
exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
h : ∀ (i : Fin 2), HDiv.hDiv (β := Fin 2 → ℤ) ((↑r : Fin 2 → ℤ) * x) (↑r : Fin 2 → ℤ) i = x i
⊢ (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x

Tactic:
ext i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
i : Fin 2
⊢ HDiv.hDiv (β := Fin 2 → ℤ) ((↑r : Fin 2 → ℤ) * x) (↑r : Fin 2 → ℤ) i = x i

Tactic:
simp_all [NeZero.ne r]

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
pos : ∀ (hr : r = 0), v = r • divIntMap (↑r : ℤ) v
neg : ∀ (hr : ¬r = 0), v = r • divIntMap (↑r : ℤ) v
⊢ v = r • divIntMap (↑r : ℤ) v

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : r = 0
⊢ (v 0).gcd (v 1) = r

Tactic:
have hv := hv.2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 r 0
hr : r = 0
hv : (v 0).gcd (v 1) = r
pos : ∀ (hv : v ∈ gammaSet 1 0 0) (hr : True) (hv : v 0 = 0 ∧ v 1 = 0), v = 0
⊢ v = r • divIntMap (↑r : ℤ) v

Tactic:
simp only [hr, Fin.isValue, Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_smul] at *

Premises used: CharP.cast_eq_zero, Int.gcd_eq_zero_iff, zero_smul, Fin.isValue
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
pos : ∀ (i : Fin 2), v i = 0 i
⊢ v = 0

Tactic:
ext i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
i : Fin 2
pos : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
pos₁ : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ v i = 0 i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hv]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hv]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
neg : ∀ (i : Fin 2), v i = (r • divIntMap (↑r : ℤ) v) i
⊢ v = r • divIntMap (↑r : ℤ) v

Tactic:
ext i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
i : Fin 2
⊢ v i = (r • divIntMap (↑r : ℤ) v) i

Tactic:
simp_all [Pi.smul_apply, divIntMap, ← Int.mul_ediv_assoc _ (gammaSet_div_gcd hv i)]

Premises used: EisensteinSeries.divIntMap, Int.mul_ediv_assoc, EisensteinSeries.gammaSet_div_gcd, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : (↑(gammaSet 1 r 0) : Type)
⊢ (↑((gammaSetDivGcdEquiv r : (a : (↑(gammaSet 1 r 0) : Type)) → (↑(gammaSet 1 1 0) : Type)) v) : Fin 2 → ℤ) =
    divIntMap (↑r : ℤ) (↑v : Fin 2 → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
apply : (y : ℕ) × { x : Fin 2 → ℤ // finGcdMap x = y } ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)
⊢ (Fin 2 → ℤ) ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)

Tactic:
apply (Equiv.sigmaFiberEquiv finGcdMap).symm.trans

Premises used: Equiv.trans, Equiv.sigmaFiberEquiv, EisensteinSeries.finGcdMap, Equiv.symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
refine : (b : ℕ) → { x : Fin 2 → ℤ // finGcdMap x = b } ≃ (↑(gammaSet 1 b 0) : Type)
⊢ (y : ℕ) × { x : Fin 2 → ℤ // finGcdMap x = y } ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)

Tactic:
refine Equiv.sigmaCongrRight fun b => ?_

Premises used: Equiv.sigmaCongrRight
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
h : Eq (α := (Fin 2 → ℤ) → Prop) (fun (x : Fin 2 → ℤ) ↦ finGcdMap x = b) fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet 1 b 0
⊢ { x : Fin 2 → ℤ // finGcdMap x = b } ≃ (↑(gammaSet 1 b 0) : Type)

Tactic:
apply Equiv.subtypeEquivProp

Premises used: Equiv.subtypeEquivProp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
⊢ Eq (α := (Fin 2 → ℤ) → Prop) (fun (x : Fin 2 → ℤ) ↦ finGcdMap x = b) fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet 1 b 0

Tactic:
simp [gammaSet_one_eq]

Premises used: EisensteinSeries.gammaSet_one_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
v : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)
⊢ (gammaSetDivGcdSigmaEquiv.symm : (a : (r : ℕ) × (↑(gammaSet 1 r 0) : Type)) → Fin 2 → ℤ) v =
    (↑(v.snd (β := fun (r : ℕ) ↦ (↑(gammaSet 1 r 0) : Type))) : Fin 2 → ℤ)

Tactic:
rfl

Premises used: Set.Mem, EisensteinSeries.gammaSet, setOf, rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
h : ∀ (i : Fin 2), v i = (r • (v / (↑r : Fin 2 → ℤ))) i
⊢ v = r • (v / (↑r : Fin 2 → ℤ))

Tactic:
ext i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ v i = (r • (v / (↑r : Fin 2 → ℤ))) i

Tactic:
Eq.symm (Int.mul_ediv_cancel' ?_)

Premises used: Int.mul_ediv_cancel', Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
h : (↑r : ℤ) ∣ v i
⊢ v i = (r • (v / (↑r : Fin 2 → ℤ))) i

Tactic:
refine Eq.symm (Int.mul_ediv_cancel' ?_)

Premises used: Int.mul_ediv_cancel', Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
h : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
h₁ : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (↑r : ℤ) ∣ v i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]

Premises used: Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]

Premises used: Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ v = r • (v / (↑r : Fin 2 → ℤ))

Tactic:
have hvr : v = r • (v / r) := by
    ext i
    refine Eq.symm (Int.mul_ediv_cancel' ?_)
    fin_cases i <;> simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / (↑r : Fin 2 → ℤ))
rw : finGcdMap (r • (v / (↑r : Fin 2 → ℤ)) ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r
⊢ finGcdMap (v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r

Tactic:
rw [hvr, smul_vecMul]

Premises used: Matrix.smul_vecMul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / (↑r : Fin 2 → ℤ))
⊢ finGcdMap (r • (v / (↑r : Fin 2 → ℤ)) ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r

Tactic:
simpa using finGcdMap_smul r (Int.isCoprime_iff_gcd_eq_one.mp ((finGcdMap_div v hab).vecMulSL A))

Premises used: Int.isCoprime_iff_gcd_eq_one, IsCoprime.vecMulSL, EisensteinSeries.finGcdMap_div, EisensteinSeries.finGcdMap_smul, Nat.cast, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ) ∈
    gammaSet N r
      (a ᵥ*
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))

Tactic:
⟨?_, vecMulSL_gcd hv.2 γ⟩

Premises used: Set.Mem, EisensteinSeries.gammaSet, setOf, And.right, And.intro, EisensteinSeries.vecMulSL_gcd
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
refine :
  Int.cast ∘ (v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) =
    a ᵥ*
      (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N))
⊢ v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ) ∈
    gammaSet N r
      (a ᵥ*
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))

Tactic:
refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ ∀ (i : Fin 2),
    Eq (α := ZMod N) ((Int.castRingHom (ZMod N) : (a : ℤ) → ZMod N) ((v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) i) : ZMod N)
      (((⇑(Int.castRingHom (ZMod N)) : (a : ℤ) → ZMod N) ∘ v ᵥ*
            (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map (⇑(Int.castRingHom (ZMod N)) : (a : ℤ) → ZMod N))
          i :
        ZMod N)

Tactic:
have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    Eq (α := ZMod N) ((Int.castRingHom (ZMod N) : (a : ℤ) → ZMod N) ((v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) i) : ZMod N)
      (((⇑(Int.castRingHom (ZMod N)) : (a : ℤ) → ZMod N) ∘ v ᵥ*
            (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map (⇑(Int.castRingHom (ZMod N)) : (a : ℤ) → ZMod N))
          i :
        ZMod N)
⊢ ∀ (i : Fin 2),
    Eq (α := ZMod N) (↑((v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) i) : ZMod N)
      (((fun (x : ℤ) ↦ (↑x : ZMod N)) ∘ v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map fun (x : ℤ) ↦ (↑x : ZMod N)) i)

Tactic:
simp only [eq_intCast, Int.coe_castRingHom] at this

Premises used: Int.coe_castRingHom, eq_intCast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    Eq (α := ZMod N) (↑((v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) i) : ZMod N)
      (((fun (x : ℤ) ↦ (↑x : ZMod N)) ∘ v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map fun (x : ℤ) ↦ (↑x : ZMod N)) i)
simp_rw :
  Eq (α := Fin 2 → ZMod N) (fun (x : Fin 2) ↦ (a ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map fun (x : ℤ) ↦ (↑x : ZMod N)) x)
    (a ᵥ*
      (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N)))
⊢ Int.cast ∘ (v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) =
    a ᵥ*
      (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N))

Tactic:
simp_rw [Function.comp_def, this, hv.1]

Premises used: Function.comp_def, And.left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    Eq (α := ZMod N) (↑((v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ)) i) : ZMod N)
      (((fun (x : ℤ) ↦ (↑x : ZMod N)) ∘ v ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map fun (x : ℤ) ↦ (↑x : ZMod N)) i)
⊢ Eq (α := Fin 2 → ZMod N) (fun (x : Fin 2) ↦ (a ᵥ* (↑γ : Matrix (Fin 2) (Fin 2) ℤ).map fun (x : ℤ) ↦ (↑x : ZMod N)) x)
    (a ᵥ*
      (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N)))

Tactic:
simp
-- 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)
⊢ (↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ∈
    gammaSet N r
      (vecMul (m := Fin 2)
        (a ᵥ*
          (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
            Matrix (Fin 2) (Fin 2) (ZMod N)))
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ⁻¹) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))

Tactic:
have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
-- 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)
this :
  (↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ∈
    gammaSet N r
      (vecMul (m := Fin 2)
        (a ᵥ*
          (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
            Matrix (Fin 2) (Fin 2) (ZMod N)))
        (↑((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) ℤ) ∈
    gammaSet N r
      (a ᵥ*
        (↑(HMul.hMul (α := SL(2, ZMod N)) (β := SL(2, ZMod N))
              ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
              ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ⁻¹ :
                SL(2, ZMod N))) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))

Tactic:
rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this

Premises used: Matrix.vecMul_vecMul, Matrix.SpecialLinearGroup.coe_mul
-- 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)
this :
  (↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ∈
    gammaSet N r
      (a ᵥ*
        (↑(HMul.hMul (α := SL(2, ZMod N)) (β := SL(2, ZMod N))
              ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
              ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ⁻¹ :
                SL(2, ZMod N))) :
          Matrix (Fin 2) (Fin 2) (ZMod N)))
⊢ (↑v : Fin 2 → ℤ) ᵥ* (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ∈ gammaSet N r a

Tactic:
simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
        map_inv, mul_inv_cancel, SpecialLinearGroup.coe_one, vecMul_one]

Premises used: RingHom.mapMatrix_apply, map_inv, Matrix.SpecialLinearGroup.coe_one, Int.coe_castRingHom, Matrix.SpecialLinearGroup.map_apply_coe, mul_inv_cancel, Matrix.vecMul_one