awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
hF : ∀ (τ : ℍ), C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖
⊢ IsBigO (E := ℂ) (F := ℝ) (comap UpperHalfPlane.im (𝓝 0)) (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦
    τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)

Tactic:
refine isBigO_of_le' (c := C) _ fun τ ↦ (hC τ).trans (of_eq ?_)

Premises used: Asymptotics.isBigO_of_le', of_eq, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
τ : ℍ
⊢ 0 ≤ τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.IsArithmetic
F : Type u_2
inst_1 : FunLike F ℍ ℂ
inst_2 : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), norm (E := ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ) ≤ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2
τ : ℍ
hF : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
hF₁ : C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹
hF₂ hF₃ : C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹ = C * (τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)⁻¹
⊢ C / τ.im ^ HDiv.hDiv (α := ℝ) (↑k : ℝ) 2 = C * ‖τ.im ^ (-HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)‖

Tactic:
rw [Real.norm_of_nonneg (by positivity), Real.rpow_neg τ.im_pos.le, div_eq_mul_inv]

Premises used: UpperHalfPlane.im_pos, LT.lt.le, div_eq_mul_inv, Real.rpow_neg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
i j : Fin 2
⊢ Eq (α := ZMod N)
    ((↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N))
      i j)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N)

Tactic:
rfl

Premises used: Matrix.map, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Γ(N) ↔
    Eq (α := SL(2, ZMod N))
      ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
      (1 : SL(2, ZMod N))

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
mp :
  Eq (α := SL(2, ZMod N))
      ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
      (1 : SL(2, ZMod N)) →
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 →
    Eq (α := SL(2, ZMod N))
      ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
      (1 : SL(2, ZMod N))
⊢ Eq (α := SL(2, ZMod N))
      ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
      (1 : SL(2, ZMod N)) ↔
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
          Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := SL(2, ZMod N))
    ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
    (1 : SL(2, ZMod N))
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1

Tactic:
simp [← SL_reduction_mod_hom_val N γ, h]

Premises used: SL_reduction_mod_hom_val
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  ∀ (i j : Fin 2),
    Eq (α := ZMod N)
      ((↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
          Matrix (Fin 2) (Fin 2) (ZMod N))
        i j)
      ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)
⊢ Eq (α := SL(2, ZMod N))
    ((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ : SL(2, ZMod N))
    (1 : SL(2, ZMod N))

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
i j : Fin 2
mpr : Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N) ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)
⊢ Eq (α := ZMod N)
    ((↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) γ) :
        Matrix (Fin 2) (Fin 2) (ZMod N))
      i j)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)

Tactic:
rw [SL_reduction_mod_hom_val N γ]

Premises used: SL_reduction_mod_hom_val
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
i j : Fin 2
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j)
mpr₁ :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j)
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N) ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
j : Fin 2
mpr :
  Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
mpr₁ :
  Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
j : Fin 2
mpr :
  Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
mpr₁ :
  Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨0, ⋯⟩ ⟨0, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨0, ⋯⟩ ⟨0, ⋯⟩)
⊢ Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨0, ⋯⟩ ⟨1, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨0, ⋯⟩ ⟨1, ⋯⟩)
⊢ Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨1, ⋯⟩ ⟨0, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨1, ⋯⟩ ⟨0, ⋯⟩)
⊢ Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
mpr :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨1, ⋯⟩ ⟨1, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨1, ⋯⟩ ⟨1, ⋯⟩)
⊢ Eq (α := ZMod N)
    (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨0, ⋯⟩ ⟨0, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨0, ⋯⟩ ⟨0, ⋯⟩)

Tactic:
h.1

Premises used: Fin.ofNat, And.left, Matrix.diagonal, ite
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨0, ⋯⟩ ⟨1, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨0, ⋯⟩ ⟨1, ⋯⟩)

Tactic:
h.2.1

Premises used: Fin.ofNat, And.right, And.left, Matrix.diagonal, ite
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨1, ⋯⟩ ⟨0, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨1, ⋯⟩ ⟨0, ⋯⟩)

Tactic:
h.2.2.1

Premises used: Fin.ofNat, And.right, And.left, Matrix.diagonal, ite
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨1, ⋯⟩ ⟨1, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨1, ⋯⟩ ⟨1, ⋯⟩)

Tactic:
h.2.2.2

Premises used: Fin.ofNat, And.right, Matrix.diagonal, ite
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : SL(2, ℤ)
h :
  Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ⟨0, ⋯⟩ ⟨0, ⋯⟩) : ZMod N)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ⟨0, ⋯⟩ ⟨0, ⋯⟩)

Tactic:
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
⊢ Γ(N).Normal

Tactic:
SLMOD(N).normal_ker

Premises used: CongruenceSubgroup.Gamma, ZMod, Matrix.SpecialLinearGroup.map, Int.castRingHom, MonoidHom.normal_ker
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
h : ∀ (x : SL(2, ℤ)), x ∈ Γ(1) ↔ Membership.mem (γ := Subgroup SL(2, ℤ)) ⊤ x
⊢ Γ(1) = ⊤

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
x : SL(2, ℤ)
⊢ x ∈ Γ(1) ↔ Membership.mem (γ := Subgroup SL(2, ℤ)) ⊤ x

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
γ : SL(2, ℤ)
⊢ γ ∈ Γ(1)

Tactic:
simp only [Gamma_one_top, Subgroup.mem_top]

Premises used: CongruenceSubgroup.Gamma_one_top, Subgroup.mem_top
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
⊢ Eq (α := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(1)) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
simp [Gamma_one_top, MonoidHom.range_eq_map]

Premises used: MonoidHom.range_eq_map, CongruenceSubgroup.Gamma_one_top
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
⊢ Γ(0) = ⊥

Tactic:
rfl

Premises used: Matrix.SpecialLinearGroup, MonoidHom.mker, Set.Mem, setOf, CongruenceSubgroup.Gamma, ZMod, MonoidHom.ker, Submonoid.comap, Set.preimage, Set.singleton, Matrix.map, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N M : ℤ
hNM : N ∣ M
simp : Eq (α := ZMod N.natAbs) (↑M : ZMod N.natAbs) 0
⊢ ModularGroup.T ^ M ∈ Γ(N.natAbs)

Tactic:
simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero,
    empty_val', cons_val_fin_one, Int.cast_one, cons_val_one,
    Int.cast_zero, and_self, and_true, true_and]

Premises used: and_true, and_self, Int.cast_zero, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.empty_val', Matrix.cons_val_fin_one, Matrix.of_apply, Fin.isValue, ModularGroup.coe_T_zpow, CongruenceSubgroup.Gamma_mem, Int.cast_one, true_and, Matrix.cons_val'
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N M : ℤ
hNM : N ∣ M
⊢ Eq (α := ZMod N.natAbs) (↑M : ZMod N.natAbs) 0

Tactic:
Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_

Premises used: Iff.mpr, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N M : ℤ
hNM : N ∣ M
refine : (↑N.natAbs : ℤ) ∣ M
⊢ Eq (α := ZMod N.natAbs) (↑M : ZMod N.natAbs) 0

Tactic:
refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_

Premises used: Iff.mpr, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N M : ℤ
hNM : N ∣ M
⊢ (↑N.natAbs : ℤ) ∣ M

Tactic:
simp only [Int.natCast_natAbs, abs_dvd, hNM]

Premises used: abs_dvd, Int.natCast_natAbs
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ Γ(N).FiniteIndex

Tactic:
Subgroup.finiteIndex_ker _

Premises used: CongruenceSubgroup.Gamma, Subgroup.finiteIndex_ker
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a b : SL(2, ℤ)
ha :
  Membership.mem (γ := Set SL(2, ℤ))
    {g : SL(2, ℤ) | Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0} a
hb :
  Membership.mem (γ := Set SL(2, ℤ))
    {g : SL(2, ℤ) | Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0} b
⊢ ((↑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

Tactic:
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a b : SL(2, ℤ)
ha : Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hb : Eq (α := ZMod N) (↑((↑b : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
h :
  ((↑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
rw :
  Eq (α := ZMod N)
    (↑((↑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) :
      ZMod N)
    0
⊢ Eq (α := ZMod N) (↑(((↑a : Matrix (Fin 2) (Fin 2) ℤ) * (↑b : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ZMod N) 0

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a b : SL(2, ℤ)
ha : Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hb : Eq (α := ZMod N) (↑((↑b : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
h :
  ((↑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
⊢ Eq (α := ZMod N)
    (↑((↑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) :
      ZMod N)
    0

Tactic:
simp [ha, hb]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
⊢ Membership.mem (γ := Set SL(2, ℤ))
    {g : SL(2, ℤ) | Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0} 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a : SL(2, ℤ)
ha :
  Membership.mem (γ := Set SL(2, ℤ))
    {g : SL(2, ℤ) | Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0} a
rw :
  Eq (α := ZMod N)
    (↑((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1)
                ![![(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 1, -(↑a : Matrix (Fin 2) (Fin 2) ℤ) 0 1],
                  ![-(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0, (↑a : Matrix (Fin 2) (Fin 2) ℤ) 0 0]]
                ⋯) :
            Matrix (Fin 2) (Fin 2) ℤ)
          1 0) :
      ZMod N)
    0
⊢ Eq (α := ZMod N) (↑((↑a⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
rw [SL2_inv_expl a]

Premises used: Matrix.SpecialLinearGroup.SL2_inv_expl
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a : SL(2, ℤ)
ha :
  Membership.mem (γ := Set SL(2, ℤ))
    {g : SL(2, ℤ) | Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0} a
simp : Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N)
    (↑((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1)
                ![![(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 1, -(↑a : Matrix (Fin 2) (Fin 2) ℤ) 0 1],
                  ![-(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0, (↑a : Matrix (Fin 2) (Fin 2) ℤ) 0 0]]
                ⋯) :
            Matrix (Fin 2) (Fin 2) ℤ)
          1 0) :
      ZMod N)
    0

Tactic:
simp only [cons_val_zero, cons_val_one,
      Int.cast_neg, neg_eq_zero, Set.mem_setOf_eq] at *

Premises used: Int.cast_neg, Matrix.cons_val_one, Matrix.cons_val_zero, neg_eq_zero, Set.mem_setOf_eq
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a : SL(2, ℤ)
ha : Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
ha
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
a : SL(2, ℤ)
ha : Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N) (↑((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
exact ha
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma0 N ↔ Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N_1 N : ℕ
⊢ Eq (α := ZMod N) (↑((↑(↑1 : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1

Tactic:
simp