awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
⊢ DifferentiableOn ℂ (F := ℂ) ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))
    {z : ℂ | 0 < z.im}
have refine : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z),
  ((⇑{ toFun := Δ, slash_action_eq' := sorry } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) z = HPow.hPow (β := ℕ) η 24 z
Tactic: refine .congr (fun z hz ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).pow
      24 |>.differentiableWithinAt) fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ c.IsZeroAt Δ 12
have rw : ∀ (γ : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
      c →
    IsZeroAtImInfty
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)
Tactic: rw [OnePoint.isZeroAt_iff_forall_SL2Z hc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
    c
⊢ IsZeroAtImInfty
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)
have rw : IsZeroAtImInfty Δ
Tactic: rw [slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic (hypothesis)
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(N))
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ) k
have hc₁ : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
Tactic: rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic (goal)
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ) k
have rw : ∀ (γ : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
      c →
    UpperHalfPlane.IsBoundedAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : UpperHalfPlane) ↦ ℂ)) _ k γ
        (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ))
Tactic: rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
⊢ Pairwise (Disjoint on gammaSet N r)
have refine : ∀ (u v : Fin 2 → ZMod N) (huv : u ≠ v), (Disjoint on gammaSet N r) u v
Tactic: refine fun u v huv ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : u ≠ v
⊢ (Disjoint on gammaSet N r) u v
have contrapose : ∀ (huv : ¬(Disjoint on gammaSet N r) u v), u = v
Tactic: contrapose huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N r) u v
⊢ u = v
have obtain : ∀ (f : Fin 2 → ℤ) (hf : f ∈ gammaSet N r u ∧ f ∈ gammaSet N r v), u = v
Tactic: obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑r : Fin 2 → ℤ) 0) (HDiv.hDiv (β := Fin 2 → ℤ) v (↑r : Fin 2 → ℤ) 1)
have rw : IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 0)
  (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 1)
Tactic: rw [← hv]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 0)
    (HDiv.hDiv (β := Fin 2 → ℤ) v (↑(finGcdMap v) : Fin 2 → ℤ) 1)
have hpq : @gcd _ CommSemiring.toCommMonoidWithZero _ (v 0) (v 1) ≠ 0
Tactic: apply isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hv : finGcdMap v = r
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (v 0) (v 1) ≠ 0
have this : r ≠ 0
Tactic: have := NeZero.ne r
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)
have rw : (v 0).gcd (v 1) = 1 ↔ IsCoprime (v 0) (v 1)
Tactic: rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
v : Fin 2 → ℤ
rw : (v 0).gcd (v 1) = 1 ↔ IsCoprime (v 0) (v 1)
⊢ v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)
have rw₁ : (v 0).gcd (v 1) = 1 ↔ (v 0).gcd (v 1) = 1
Tactic: rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
i : Fin 2
⊢ (↑r : ℤ) ∣ v i
have 0 : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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))
⊢ (↑r : ℤ) ∣ v i
have 1 : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
⊢ BijOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
have refine_1 : MapsTo (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
refine_1 : MapsTo (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
⊢ BijOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
have refine_2 : InjOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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)
⊢ BijOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
have refine_3 : SurjOn (divIntMap (↑r : ℤ)) (gammaSet 1 r 0) (gammaSet 1 1 0)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ divIntMap (↑r : ℤ) x ∈ gammaSet 1 1 0
have refine_1 : IsCoprime (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 0)
  (HDiv.hDiv (β := Fin 2 → ℤ) x (↑(↑r : ℤ) : Fin 2 → ℤ) 1)
Tactic: simp only [divIntMap, mem_gammaSet_one] at *
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
⊢ x = v
have refine_2 : ∀ (i : Fin 2), x i = v i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ x ∈ divIntMap (↑r : ℤ) '' gammaSet 1 r 0
have h : r • x ∈ gammaSet 1 r 0 ∧ divIntMap (↑r : ℤ) (r • x) = x
Tactic: use r • x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0 ∧ (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x
have h : (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
h : (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0
⊢ (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0 ∧ (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x
have h₁ : (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ (↑r : Fin 2 → ℤ) * x ∈ gammaSet 1 r 0
have hx₁ : (x 0).gcd (x 1) = 1
Tactic: rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ (↑r : Fin 2 → ℤ) * x / (↑r : Fin 2 → ℤ) = x
have h : ∀ (i : Fin 2), HDiv.hDiv (β := Fin 2 → ℤ) ((↑r : Fin 2 → ℤ) * x) (↑r : Fin 2 → ℤ) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ v = r • divIntMap (↑r : ℤ) v
have pos : ∀ (hr : r = 0), v = r • divIntMap (↑r : ℤ) v
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
pos : ∀ (hr : r = 0), v = r • divIntMap (↑r : ℤ) v
⊢ v = r • divIntMap (↑r : ℤ) v
have neg : ∀ (hr : ¬r = 0), v = r • divIntMap (↑r : ℤ) v
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : r = 0
⊢ v = r • divIntMap (↑r : ℤ) v
have hv₁ : (v 0).gcd (v 1) = r
Tactic: have hv := hv.2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 r 0
hr : r = 0
hv : (v 0).gcd (v 1) = r
⊢ v = r • divIntMap (↑r : ℤ) v
have pos : ∀ (hv : v ∈ gammaSet 1 0 0) (hr : True) (hv : v 0 = 0 ∧ v 1 = 0), v = 0
Tactic: simp only [hr, Fin.isValue, Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_smul] at *
Cleared hypotheses: hv_1, hr, hv
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v = 0
have pos : ∀ (i : Fin 2), v i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv_1 : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
i : Fin 2
⊢ v i = 0 i
have pos : v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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, ⋯⟩)
⊢ v i = 0 i
have pos₁ : v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = 0 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r : ℤ) v
have neg : ∀ (i : Fin 2), v i = (r • divIntMap (↑r : ℤ) v) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
a : Fin 2 → ZMod N
⊢ (Fin 2 → ℤ) ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)
have apply : (y : ℕ) × { x : Fin 2 → ℤ // finGcdMap x = y } ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)
Tactic: apply (Equiv.sigmaFiberEquiv finGcdMap).symm.trans
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
a : Fin 2 → ZMod N
⊢ (y : ℕ) × { x : Fin 2 → ℤ // finGcdMap x = y } ≃ (r : ℕ) × (↑(gammaSet 1 r 0) : Type)
have refine : (b : ℕ) → { x : Fin 2 → ℤ // finGcdMap x = b } ≃ (↑(gammaSet 1 b 0) : Type)
Tactic: refine Equiv.sigmaCongrRight fun b => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
⊢ { x : Fin 2 → ℤ // finGcdMap x = b } ≃ (↑(gammaSet 1 b 0) : Type)
have h : Eq (α := (Fin 2 → ℤ) → Prop) (fun (x : Fin 2 → ℤ) ↦ finGcdMap x = b) fun (x : Fin 2 → ℤ) ↦ x ∈ gammaSet 1 b 0
Tactic: apply Equiv.subtypeEquivProp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ v = r • (v / (↑r : Fin 2 → ℤ))
have h : ∀ (i : Fin 2), v i = (r • (v / (↑r : Fin 2 → ℤ))) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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
have h : (↑r : ℤ) ∣ v i
Tactic: refine Eq.symm (Int.mul_ediv_cancel' ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ (↑r : ℤ) ∣ v i
have h : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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))
⊢ (↑r : ℤ) ∣ v i
have h₁ : (↑r : ℤ) ∣ v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ finGcdMap (v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r
have hvr : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
Goal:
r : ℕ
inst : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / (↑r : Fin 2 → ℤ))
⊢ finGcdMap (v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r
have rw : finGcdMap (r • (v / (↑r : Fin 2 → ℤ)) ᵥ* (↑A : Matrix (Fin 2) (Fin 2) ℤ)) = r
Tactic: rw [hvr, smul_vecMul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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)))
have 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))
Tactic: refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
Goal:
N r : ℕ
a : Fin 2 → ZMod N
inst : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ 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))
have 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)
Tactic: have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
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)
⊢ 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))
have 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)
Tactic: simp only [eq_intCast, Int.coe_castRingHom] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (goal)
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)
⊢ 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))
have 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)))
Tactic: simp_rw [Function.comp_def, this, hv.1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
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 a
have 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)))
Tactic: have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs (hypothesis)
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
have 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)))
Tactic: rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this
Cleared hypotheses: this
-- 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)
⊢ (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) ℤ) ᵥ* (↑γ⁻¹ : 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
⊢ (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) ℤ) * (↑γ⁻¹ : Matrix (Fin 2) (Fin 2) ℤ))) sorry =
  v
Tactic: simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]