awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
x : SL(2, ℤ)
HA :
  Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
HA.2.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
x : SL(2, ℤ)
HA :
  Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N) (↑((↑x : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
exact HA.2.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
obtain : ∀ (N : ℕ) (hN : N ≠ 0 ∧ Γ(N) ≤ H), IsCongruenceSubgroup K
⊢ IsCongruenceSubgroup K

Tactic:
obtain ⟨N, hN⟩ := h2
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ H
⊢ IsCongruenceSubgroup K

Tactic:
⟨N, hN.1, hN.2.trans h⟩

Premises used: And.right, And.left, And.intro, Exists.intro, CongruenceSubgroup.IsCongruenceSubgroup, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ H
⊢ IsCongruenceSubgroup K

Tactic:
exact ⟨N, hN.1, hN.2.trans h⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ IsCongruenceSubgroup Γ(N)

Tactic:
⟨N, NeZero.ne _, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro, CongruenceSubgroup.IsCongruenceSubgroup, NeZero.ne
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ IsCongruenceSubgroup (Gamma1 N)

Tactic:
⟨N, NeZero.ne _, fun A hA ↦ ?_⟩

Premises used: And.intro, Exists.intro, CongruenceSubgroup.IsCongruenceSubgroup, NeZero.ne
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
refine : ∀ (A : SL(2, ℤ)) (hA : A ∈ Γ(N)), A ∈ Gamma1 N
⊢ IsCongruenceSubgroup (Gamma1 N)

Tactic:
refine ⟨N, NeZero.ne _, fun A hA ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
A : SL(2, ℤ)
hA : A ∈ Γ(N)
⊢ A ∈ Gamma1 N

Tactic:
simp_all [Gamma1_mem, Gamma_mem]

Premises used: CongruenceSubgroup.Gamma1_mem, CongruenceSubgroup.Gamma_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ IsCongruenceSubgroup (Gamma0 N)

Tactic:
isCongruenceSubgroup_trans _ _ (Gamma1_in_Gamma0 N) (Gamma1_is_congruence N)

Premises used: CongruenceSubgroup.Gamma1_in_Gamma0, CongruenceSubgroup.Gamma1_is_congruence, CongruenceSubgroup.isCongruenceSubgroup_trans
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
obtain : ∀ (N : ℕ) (hN : N ≠ 0 ∧ Γ(N) ≤ Γ), Γ.FiniteIndex
⊢ Γ.FiniteIndex

Tactic:
obtain ⟨N, hN⟩ := h
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ NeZero N

Tactic:
have : NeZero N := ⟨hN.1⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ Γ
this : NeZero N
⊢ Γ.FiniteIndex

Tactic:
Subgroup.finiteIndex_of_le hN.2

Premises used: Subgroup.finiteIndex_of_le, And.right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ Γ
this : NeZero N
⊢ Γ.FiniteIndex

Tactic:
exact Subgroup.finiteIndex_of_le hN.2

Premises used: Subgroup.finiteIndex_of_le, And.right
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ (Gamma0 N).FiniteIndex

Tactic:
(Gamma0_is_congruence N).finiteIndex

Premises used: CongruenceSubgroup.Gamma0_is_congruence, CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
inst : NeZero N
⊢ (Gamma1 N).FiniteIndex

Tactic:
(Gamma1_is_congruence N).finiteIndex

Premises used: CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex, CongruenceSubgroup.Gamma1_is_congruence
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℝ
x : SL(2, ℤ)
⊢ x ∈ conjGL Γ g ↔
    ∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ) g
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ) *
          g⁻¹

Tactic:
simp [conjGL, mapGL, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]

Premises used: ConjAct.toConjAct_smul, CongruenceSubgroup.conjGL, Subgroup.mem_inv_pointwise_smul_iff, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
h :
  ∀ (x : SL(2, ℤ)),
    x ∈
        conjGL Γ
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g)) ↔
      x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
⊢ conjGL Γ
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g)) =
    HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Γ(N) = Γ(N)

Tactic:
apply Subgroup.Normal.conjAct (Gamma_normal N)

Premises used: CongruenceSubgroup.Gamma_normal, Subgroup.Normal.conjAct
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
obtain : ∀ (N : ℕ) (HN : N ≠ 0 ∧ Γ(N) ≤ Γ), IsCongruenceSubgroup (g • Γ)
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
obtain ⟨N, HN⟩ := h
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
⟨N, ?_⟩

Premises used: Exists.intro, CongruenceSubgroup.IsCongruenceSubgroup
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
refine : N ≠ 0 ∧ Γ(N) ≤ g • Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
refine ⟨N, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN rw : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ N ≠ 0 ∧ Γ(N) ≤ g • Γ

Tactic:
rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]

Premises used: Subgroup.pointwise_smul_le_pointwise_smul_iff, CongruenceSubgroup.Gamma_cong_eq_self
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ N ≠ 0 ∧ Γ(N) ≤ Γ

Tactic:
HN
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ N ≠ 0 ∧ Γ(N) ≤ Γ

Tactic:
exact HN
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
⊢ A₁ * A₂ = 1

Tactic:
simp only [← Matrix.GeneralLinearGroup.coe_mul,
    mul_inv_cancel, Matrix.GeneralLinearGroup.coe_one, A₁, A₂]

Premises used: Matrix.GeneralLinearGroup.coe_one, mul_inv_cancel, Matrix.GeneralLinearGroup.coe_mul
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
⊢ A₁ * A₂ = 1

Tactic:
have hA₁₂ : A₁ * A₂ = 1 := by simp only [← Matrix.GeneralLinearGroup.coe_mul,
    mul_inv_cancel, Matrix.GeneralLinearGroup.coe_one, A₁, A₂]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
⊢ ∃ (N : ℕ),
    N ≠ 0 ∧
      ∀ x ∈ Γ(N),
        Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
          (HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹)

Tactic:
⟨a₁ * a₂ * M, mul_ne_zero (mul_ne_zero A₁.den_ne_zero A₂.den_ne_zero) (NeZero.ne _),
    fun ⟨y, hy⟩ hy' ↦ ?_⟩

Premises used: HMul.hMul, Subgroup.map, Rat, CongruenceSubgroup.Gamma, Membership.mem, Matrix.den_ne_zero, _private.0.CongruenceSubgroup.exists_Gamma_le_conj.match_1, Inv.inv, And.intro, Exists.intro, mul_ne_zero, Matrix.SpecialLinearGroup.mapGL, DFunLike.coe, NeZero.ne
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
refine :
  ∀ (x : SL(2, ℤ)) (y : Matrix (Fin 2) (Fin 2) ℤ) (hy : y.det = 1)
    (hy' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
      (HMul.hMul (β := GL (Fin 2) ℚ) g
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ)
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy) :
            GL (Fin 2) ℚ) *
        g⁻¹)
⊢ ∃ (N : ℕ),
    N ≠ 0 ∧
      ∀ x ∈ Γ(N),
        Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
          (HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹)

Tactic:
refine ⟨a₁ * a₂ * M, mul_ne_zero (mul_ne_zero A₁.den_ne_zero A₂.den_ne_zero) (NeZero.ne _),
    fun ⟨y, hy⟩ hy' ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))
    (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod (a₁ * a₂ * M))) : (a : SL(2, ℤ)) → SL(2, ZMod (a₁ * a₂ * M)))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy)) :
      Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))

Tactic:
rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'

Premises used: CongruenceSubgroup.Gamma_mem', Subtype.ext_iff
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' :
  Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))
    (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod (a₁ * a₂ * M))) : (a : SL(2, ℤ)) → SL(2, ZMod (a₁ * a₂ * M)))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy)) :
      Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M)))
⊢ Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1

Tactic:
simpa using hy'
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1

Tactic:
replace hy' : y.map (Int.cast : ℤ → ZMod (a₁ * a₂ * M)) = 1 := by
      rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
      simpa using hy'
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
h :
  y =
    1 +
      HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
        ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
            HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
          Matrix (Fin 2) (Fin 2) ℤ)
⊢ ∃ (k : Matrix (Fin 2) (Fin 2) ℤ), y = 1 + (a₁ * a₂ * M) • k

Tactic:
use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)

Premises used: HMul.hMul, Matrix.of, HSub.hSub, HDiv.hDiv, Nat.cast, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
h :
  y - 1 =
    HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
      ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
          HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
        Matrix (Fin 2) (Fin 2) ℤ)
⊢ y =
    1 +
      HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
        ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
            HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
          Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
rw [← sub_eq_iff_eq_add']

Premises used: sub_eq_iff_eq_add'
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
h :
  ∀ (i j : Fin 2),
    HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j =
      HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
        ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
            HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
          Matrix (Fin 2) (Fin 2) ℤ)
        i j
⊢ y - 1 =
    HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
      ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
          HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
        Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
h :
  HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j =
    HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) *
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)))
⊢ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j =
    HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℤ) (a₁ * a₂ * M)
      ((of : (a : Fin 2 → Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℤ) fun (i j : Fin 2) ↦
          HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)) :
        Matrix (Fin 2) (Fin 2) ℤ)
      i j

Tactic:
simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]

Premises used: Matrix.smul_apply, Matrix.of_apply, Nat.cast_mul, nsmul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
⊢ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j =
    HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) *
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)))

Tactic:
(Int.mul_ediv_cancel_of_dvd ?_).symm

Premises used: Int.mul_ediv_cancel_of_dvd, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
h : HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j
⊢ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j =
    HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) *
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j / (HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ)))

Tactic:
refine (Int.mul_ediv_cancel_of_dvd ?_).symm

Premises used: Int.mul_ediv_cancel_of_dvd, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
⊢ Eq (α := ZMod (a₁ * a₂ * M)) (↑0 : ZMod (a₁ * a₂ * M)) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
⊢ Eq (α := ZMod (a₁ * a₂ * M)) (↑1 : ZMod (a₁ * a₂ * M)) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : HSub.hSub (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) (Matrix.map 1 Int.cast) = 0
i j : Fin 2
⊢ ∀ (a₁_1 a₂_1 : ℤ),
    (↑(a₁_1 - a₂_1) : ZMod (a₁ * a₂ * M)) =
      HSub.hSub (α := ZMod (a₁ * a₂ * M)) (↑a₁_1 : ZMod (a₁ * a₂ * M)) (↑a₂_1 : ZMod (a₁ * a₂ * M))

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
h :
  ∀ (hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) ((y - 1).map Int.cast) 0) (i j : Fin 2),
    HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j
⊢ HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j

Tactic:
rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'

Premises used: Int.cast, sub_eq_zero, Matrix.map_sub, Matrix.map_one
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) ((y - 1).map Int.cast) 0
i j : Fin 2
⊢ HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j

Tactic:
simpa only [Matrix.zero_apply, Matrix.map_apply, ZMod.intCast_zmod_eq_zero_iff_dvd,
      Nat.cast_mul] using congr_fun₂ hy' i j

Premises used: Matrix.zero_apply, Matrix.map_apply, congr_fun₂, ZMod.intCast_zmod_eq_zero_iff_dvd, Nat.cast_mul
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := (↑g : Matrix (Fin 2) (Fin 2) ℚ)
A₂ : Matrix (Fin 2) (Fin 2) ℚ := (↑g⁻¹ : Matrix (Fin 2) (Fin 2) ℚ)
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
obtain :
  ∀ (k : Matrix (Fin 2) (Fin 2) ℤ) (hk : y = 1 + (a₁ * a₂ * M) • k),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
      (HMul.hMul (β := GL (Fin 2) ℚ) g
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ)
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy) :
            GL (Fin 2) ℚ) *
        g⁻¹)
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℚ)) (Subgroup.map (mapGL ℚ) Γ(M))
    (HMul.hMul (β := GL (Fin 2) ℚ) g
        ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ)
            (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy) :
          GL (Fin 2) ℚ) *
      g⁻¹)

Tactic:
obtain ⟨k, hk⟩ : ∃ k, y = 1 + (a₁ * a₂ * M) • k := by
    replace hy' : y.map (Int.cast : ℤ → ZMod (a₁ * a₂ * M)) = 1 := by
      rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
      simpa using hy'
    use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)
    rw [← sub_eq_iff_eq_add']
    ext i j
    simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]
    refine (Int.mul_ediv_cancel_of_dvd ?_).symm
    rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'
    simpa only [Matrix.zero_apply, Matrix.map_apply, ZMod.intCast_zmod_eq_zero_iff_dvd,
      Nat.cast_mul] using congr_fun₂ hy' i j

Premises used: HMul.hMul