awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
simp : (M • (A₁.num * k * A₂.num)).map Int.cast = A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂
⊢ z.map Int.cast = A₁ * y.map Int.cast * A₂

Tactic:
simp only [Matrix.map_add _ Int.cast_add, Matrix.map_one _ Int.cast_zero Int.cast_one, hk,
      mul_add, mul_one, add_mul, hA₁₂, add_right_inj, z]

Premises used: add_mul, Int.cast_zero, Matrix.map_one, Int.cast_add, Matrix.map_add, mul_add, mul_one, add_right_inj, Int.cast_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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ ∀ (a : ℤ), (↑((a₁ * a₂ * M) • a) : ℚ) = HSMul.hSMul (β := ℚ) (a₁ * a₂ * M) (↑a : ℚ)

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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
rw :
  HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
      HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
    HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)
| A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂

Tactic:
rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]

Premises used: Matrix.inv_denom_smul_num, Matrix.map_smul
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
conv_rhs :
  (M • (A₁.num * k * A₂.num)).map Int.cast =
    HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
        HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
      HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)
⊢ (M • (A₁.num * k * A₂.num)).map Int.cast = A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂

Tactic:
conv_rhs => rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]

Premises used: Matrix.inv_denom_smul_num, Matrix.map_smul
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ ∀ (a : ℤ), (↑(M • a) : ℚ) = HSMul.hSMul (β := ℚ) M (↑a : ℚ)

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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
simp :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
⊢ (M • (A₁.num * k * A₂.num)).map Int.cast =
    HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
        HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
      HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)

Tactic:
simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]

Premises used: Int.cast, Matrix.mul_smul, Matrix.map_mul_intCast, Matrix.smul_mul, Matrix.map_smul
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ z.map Int.cast = A₁ * y.map Int.cast * A₂

Tactic:
have hz_coe : z.map Int.cast = A₁ * (y.map Int.cast) * A₂ := by
    simp only [Matrix.map_add _ Int.cast_add, Matrix.map_one _ Int.cast_zero Int.cast_one, hk,
      mul_add, mul_one, add_mul, hA₁₂, add_right_inj, z]
    conv_rhs => rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]
    simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]
    rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
⊢ det (z.map Int.cast) = (A₁ * y.map Int.cast * A₂).det

Tactic:
have := congr_arg Matrix.det hz_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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : det (z.map Int.cast) = (A₁ * y.map Int.cast * A₂).det
⊢ (↑z.det : ℚ) = A₁.det * (↑y.det : ℚ) * A₂.det

Tactic:
simp_rw [Matrix.det_mul, ← Int.cast_det] at this

Premises used: Int.cast_det, Matrix.det_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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : (↑z.det : ℚ) = A₁.det * (↑y.det : ℚ) * A₂.det
rwa : ∀ (this : (↑z.det : ℚ) = A₁.det * A₂.det * (↑y.det : ℚ)), z.det = 1
rwa₁ : ∀ (this : (↑z.det : ℚ) = (A₁ * A₂).det * (↑y.det : ℚ)), z.det = 1
rwa₂ : ∀ (this : (↑z.det : ℚ) = HMul.hMul (α := ℚ) (det (n := Fin 2) 1) (↑y.det : ℚ)), z.det = 1
rwa₃ : ∀ (this : (↑z.det : ℚ) = HMul.hMul (α := ℚ) 1 (↑y.det : ℚ)), z.det = 1
rwa₄ : ∀ (this : Eq (α := ℚ) (↑z.det : ℚ) (↑y.det : ℚ)), z.det = 1
rwa₅ : ∀ (this : Eq (α := ℚ) (↑z.det : ℚ) (↑1 : ℚ)), z.det = 1
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (this : z.det = 1), z.det = 1
⊢ z.det = 1

Tactic:
rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this

Premises used: Int.cast_inj, Matrix.det_mul, mul_right_comm, Matrix.det_one, one_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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
⊢ z.det = 1

Tactic:
have hz_det : z.det = 1 := by
    have := congr_arg Matrix.det hz_coe
    simp_rw [Matrix.det_mul, ← Int.cast_det] at this
    rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this
-- 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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
⊢ (mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det) =
    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:
simpa only [Subtype.ext_iff, Subgroup.coe_mul, Units.ext_iff,
    Units.val_mul] using hz_coe

Premises used: Units.ext_iff, Subtype.ext_iff, Subgroup.coe_mul, Units.val_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)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
refine : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det ∈ (↑Γ(M) : Set SL(2, ℤ))
⊢ 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:
refine ⟨⟨z, hz_det⟩, ?_, by simpa only [Subtype.ext_iff, Subgroup.coe_mul, Units.ext_iff,
    Units.val_mul] using hz_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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
rw :
  Eq (α := Matrix (Fin 2) (Fin 2) (ZMod M))
    (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M)) : (a : SL(2, ℤ)) → SL(2, ZMod M))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det)) :
      Matrix (Fin 2) (Fin 2) (ZMod M))
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M))
⊢ Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det ∈ (↑Γ(M) : Set SL(2, ℤ))

Tactic:
rw [SetLike.mem_coe, CongruenceSubgroup.Gamma_mem', Subtype.ext_iff]

Premises used: CongruenceSubgroup.Gamma_mem', Subtype.ext_iff, SetLike.mem_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' : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) y hy ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
a :
  ∀ (i j : Fin 2),
    Eq (α := ZMod M)
      ((↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M)) : (a : SL(2, ℤ)) → SL(2, ZMod M))
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det)) :
          Matrix (Fin 2) (Fin 2) (ZMod M))
        i j)
      ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) (ZMod M))
    (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M)) : (a : SL(2, ℤ)) → SL(2, ZMod M))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det)) :
      Matrix (Fin 2) (Fin 2) (ZMod M))
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M))

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
obtain :
  ∀ (N : ℕ) (hN : N ≠ 0)
    (h :
      ∀ 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⁻¹)),
    ∃ (N : ℕ),
      N ≠ 0 ∧
        HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
            ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
                ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
              ConjAct (GL (Fin 2) ℝ))
            (Subgroup.map (mapGL ℝ) Γ(N)) ≤
          Subgroup.map (mapGL ℝ) Γ(M)
⊢ ∃ (N : ℕ),
    N ≠ 0 ∧
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
obtain ⟨N, hN, h⟩ := exists_Gamma_le_conj g M

Premises used: CongruenceSubgroup.exists_Gamma_le_conj
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ 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⁻¹)
⊢ ∃ (N : ℕ),
    N ≠ 0 ∧
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
⟨N, hN, fun y hy ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ 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⁻¹)
refine :
  ∀ (y : GL (Fin 2) ℝ)
    (hy :
      y ∈
        HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N))),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M)) y
⊢ ∃ (N : ℕ),
    N ≠ 0 ∧
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (mapGL ℝ) Γ(N)) ≤
        Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
refine ⟨N, hN, fun y hy ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ 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⁻¹)
y : GL (Fin 2) ℝ
hy :
  y ∈
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N))
⊢ ∃ x ∈ Γ(N),
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ) =
      y

Tactic:
simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.mem_map,
    eq_inv_smul_iff] at hy

Premises used: Subgroup.mem_map, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, eq_inv_smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ 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⁻¹)
y : GL (Fin 2) ℝ
hy :
  ∃ x ∈ Γ(N),
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ) =
      y
obtain :
  ∀ (x : SL(2, ℤ)) (hx : x ∈ Γ(N)),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M))
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M)) y

Tactic:
obtain ⟨x, hx, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero M
N : ℕ
hN : N ≠ 0
h :
  ∀ 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⁻¹)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
obtain :
  ∀ (z : SL(2, ℤ)) (hz : z ∈ (↑Γ(M) : Set SL(2, ℤ)))
    (hz' :
      (mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) z =
        HMul.hMul (β := GL (Fin 2) ℚ) g ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) x : GL (Fin 2) ℚ) * g⁻¹),
    Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M))
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (mapGL ℝ) Γ(M))
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))

Tactic:
obtain ⟨z, hz, hz'⟩ := h x hx