awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N_1 N : ℕ
A : SL(2, ℤ)
hA : A ∈ Gamma0 N
B : SL(2, ℤ)
property : B ∈ Gamma0 N
⊢ (↑((↑(↑(Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA *
                    Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) B property) :
                SL(2, ℤ)) :
            Matrix (Fin 2) (Fin 2) ℤ)
          1 1) :
      ZMod N) =
    HMul.hMul (α := ZMod N)
      (↑((↑(↑(Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA) : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) :
        ZMod N)
      (↑((↑(↑(Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) B property) : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1
            1) :
        ZMod N)

Tactic:
simp only [MulMemClass.mk_mul_mk, Fin.isValue, coe_mul, (two_mul_expl A.1 B).2.2.2,
      Int.cast_add, Int.cast_mul, Gamma0_mem.mp hA, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, Int.cast_add, zero_add, Int.cast_mul, And.right, Fin.isValue, Iff.mp, Matrix.two_mul_expl, MulMemClass.mk_mul_mk, Subtype.val, Matrix.SpecialLinearGroup.coe_mul, CongruenceSubgroup.Gamma0_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
γ : ↥(Gamma0 N)
⊢ γ ∈ Gamma1' N ↔ Eq (α := ZMod N) ((Gamma0Map N : (a : ↥(Gamma0 N)) → ZMod N) γ : ZMod N) (1 : ZMod N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
mp :
  A ∈ Gamma1' N →
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
mpr :
  Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 →
    A ∈ Gamma1' N
⊢ A ∈ Gamma1' N ↔
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ Eq (α := ZMod N) (↑(↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ).det : ZMod N) 1

Tactic:
simp only [A.1.property, Int.cast_one]

Premises used: Subtype.val, Int.cast_one, Subtype.property
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ Eq (α := ZMod N) (↑(↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ).det : ZMod N) 1

Tactic:
have adet : (A.1.1.det : ZMod N) = 1 := by simp only [A.1.property, Int.cast_one]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
adet : Eq (α := ZMod N) (↑(↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ).det : ZMod N) 1
⊢ Eq (α := ZMod N)
    (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
          (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) :
      ZMod N)
    1

Tactic:
rw [Matrix.det_fin_two] at adet

Premises used: Matrix.det_fin_two
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
adet :
  Eq (α := ZMod N)
    (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
          (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) :
      ZMod N)
    1
⊢ Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1

Tactic:
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul] at *

Premises used: Int.cast_sub, CongruenceSubgroup.Gamma1_mem', OneHom.coe_mk, Int.cast_mul, MonoidHom.coe_mk, CongruenceSubgroup.Gamma0Map
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
adet :
  Eq (α := ZMod N)
    (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1 -
          (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 1 * (↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) :
      ZMod N)
    1
ha₁ : Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
⊢ HMul.hMul (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N)
        (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) -
      HMul.hMul (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N)
        (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) =
    1

Tactic:
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul] at *

Premises used: Int.cast_sub, CongruenceSubgroup.Gamma1_mem', OneHom.coe_mk, Int.cast_mul, MonoidHom.coe_mk, CongruenceSubgroup.Gamma0Map
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1
adet :
  HMul.hMul (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N)
        (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) -
      HMul.hMul (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N)
        (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) =
    1
⊢ Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul, ha, Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero,
      sub_zero] using adet

Premises used: and_true, sub_zero, Int.cast_sub, CongruenceSubgroup.Gamma1_mem', OneHom.coe_mk, MulZeroClass.mul_zero, Int.cast_mul, MonoidHom.coe_mk, Iff.mp, and_self_iff, mul_one, Subtype.property, CongruenceSubgroup.Gamma0Map, CongruenceSubgroup.Gamma0_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha :
  Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
mpr :
  Eq (α := ZMod N)
    (({ toFun := fun (g : ↥(Gamma0 N)) ↦ (↑((↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N),
            map_one' := ⋯ } :
          (a : ↥(Gamma0 N)) → ZMod N)
        A :
      ZMod N)
    (1 : ZMod N)
⊢ A ∈ Gamma1' N

Tactic:
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk]

Premises used: CongruenceSubgroup.Gamma1_mem', MonoidHom.coe_mk, CongruenceSubgroup.Gamma0Map
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha :
  Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N)
    (({ toFun := fun (g : ↥(Gamma0 N)) ↦ (↑((↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N),
            map_one' := ⋯ } :
          (a : ↥(Gamma0 N)) → ZMod N)
        A :
      ZMod N)
    (1 : ZMod N)

Tactic:
ha.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha :
  Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑A : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N)
    (({ toFun := fun (g : ↥(Gamma0 N)) ↦ (↑((↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N),
            map_one' := ⋯ } :
          (a : ↥(Gamma0 N)) → ZMod N)
        A :
      ZMod N)
    (1 : ZMod N)

Tactic:
exact ha.2.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
mp :
  A ∈ Gamma1 N →
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
mpr :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 →
    A ∈ Gamma1 N
⊢ A ∈ Gamma1 N ↔
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha : A ∈ Gamma1 N
⊢ ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A

Tactic:
simp_rw [Gamma1, Subgroup.mem_map] at ha

Premises used: Subgroup.mem_map, CongruenceSubgroup.Gamma1
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A
mp :
  ∀ (x : ↥(Gamma0 N)) (hx : x ∈ Gamma1' N)
    (hxx :
      Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) ∧
        ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
            (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) =
          A),
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
        Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
obtain ⟨⟨x, hx⟩, hxx⟩ := ha
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx : x ∈ Gamma1' N
hxx :
  Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) =
      A
⊢ Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
rw [Gamma1_to_Gamma0_mem] at hx

Premises used: CongruenceSubgroup.Gamma1_to_Gamma0_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx : x ∈ Gamma1' N
hxx :
  Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) =
      A
hx₁ :
  Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx) =
      A

Tactic:
rw [Gamma1_to_Gamma0_mem] at hx

Premises used: CongruenceSubgroup.Gamma1_to_Gamma0_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx_1 : x ∈ Gamma1' N
hx :
  Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hxx :
  Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) =
      A
⊢ ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) =
    A

Tactic:
simp only [Subgroup.mem_top, true_and] at hxx

Premises used: Subgroup.mem_top, true_and
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx_1 : x ∈ Gamma1' N
hx :
  Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hxx :
  ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) =
    A
mp :
  Eq (α := ZMod N)
      (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                  (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
              Matrix (Fin 2) (Fin 2) ℤ)
            0 0) :
        ZMod N)
      1 ∧
    Eq (α := ZMod N)
        (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                    (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
                Matrix (Fin 2) (Fin 2) ℤ)
              1 1) :
          ZMod N)
        1 ∧
      Eq (α := ZMod N)
        (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                    (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
                Matrix (Fin 2) (Fin 2) ℤ)
              1 0) :
          ZMod N)
        0
⊢ Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
rw [← hxx]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx_1 : x ∈ Gamma1' N
hx :
  Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hxx :
  ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) =
    A
⊢ Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0

Tactic:
hx
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx_1 : x ∈ Gamma1' N
hx :
  Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑(↑x : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hxx :
  ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1) =
    A
⊢ Eq (α := ZMod N)
      (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                  (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
              Matrix (Fin 2) (Fin 2) ℤ)
            0 0) :
        ZMod N)
      1 ∧
    Eq (α := ZMod N)
        (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                    (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
                Matrix (Fin 2) (Fin 2) ℤ)
              1 1) :
          ZMod N)
        1 ∧
      Eq (α := ZMod N)
        (↑((↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
                    (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N) x hx_1)) :
                Matrix (Fin 2) (Fin 2) ℤ)
              1 0) :
          ZMod N)
        0

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

Tactic:
simp [ha.right.right, Gamma0_mem]

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

Tactic:
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
simp :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
⊢ Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA ∈ Gamma1' N

Tactic:
simp only [Gamma1_to_Gamma0_mem]

Premises used: CongruenceSubgroup.Gamma1_to_Gamma0_mem
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
⊢ Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      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) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
⊢ Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      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, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
⊢ Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA ∈ Gamma1' N

Tactic:
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N := by
      simp only [Gamma1_to_Gamma0_mem]
      exact ha
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
HA : Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA ∈ Gamma1' N
⊢ ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A

Tactic:
⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), ?_⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
HA : Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA ∈ Gamma1' N
mpr :
  Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N)
        (Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA) HA) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N)
          (Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA) HA) =
      A
⊢ ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A

Tactic:
refine ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
A : SL(2, ℤ)
ha :
  Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1 ∧
      Eq (α := ZMod N) (↑((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
hA : A ∈ Gamma0 N
HA : Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA ∈ Gamma1' N
⊢ Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤
      (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N)
        (Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA) HA) ∧
    ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ))
        (Subtype.mk (p := fun (x : ↥(Gamma0 N)) ↦ x ∈ Gamma1' N)
          (Subtype.mk (p := fun (x : SL(2, ℤ)) ↦ x ∈ Gamma0 N) A hA) HA) =
      A

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
simp :
  ∀
    (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
⊢ x ∈ Gamma0 N

Tactic:
simp only [Gamma0_mem, Gamma1_mem] at *

Premises used: CongruenceSubgroup.Gamma1_mem, CongruenceSubgroup.Gamma0_mem