awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N : ℕ
γ : SL(2, ℤ)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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 (α := 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))
have 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)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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)
have mpr : Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N) ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)
Tactic: rw [SL_reduction_mod_hom_val N γ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N) ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)
have mpr : Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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)
⊢ Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) i j) : ZMod N) ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) i j)
have mpr₁ : Eq (α := ZMod N) (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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)
have mpr : Eq (α := ZMod N)
  (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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, ⋯⟩))
⊢ 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)
have mpr₁ : Eq (α := ZMod N)
  (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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)
have mpr : Eq (α := ZMod N)
  (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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, ⋯⟩))
⊢ 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)
have mpr₁ : Eq (α := ZMod N)
  (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) : ZMod N)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod N)) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
⊢ Γ(1) = ⊤
have h : ∀ (x : SL(2, ℤ)), x ∈ Γ(1) ↔ Membership.mem (γ := Subgroup SL(2, ℤ)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N M : ℤ
hNM : N ∣ M
⊢ ModularGroup.T ^ M ∈ Γ(N.natAbs)
have simp : Eq (α := ZMod N.natAbs) (↑M : ZMod N.natAbs) 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N M : ℤ
hNM : N ∣ M
⊢ Eq (α := ZMod N.natAbs) (↑M : ZMod N.natAbs) 0
have refine : (↑N.natAbs : ℤ) ∣ M
Tactic: refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
⊢ Eq (α := ZMod N) (↑((↑(a * b) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
have 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
Tactic: have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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) ℤ) * (↑b : Matrix (Fin 2) (Fin 2) ℤ)) 1 0) : ZMod N) 0
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ Eq (α := ZMod N) (↑((↑a⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0
have 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]]
              sorry) :
          Matrix (Fin 2) (Fin 2) ℤ)
        1 0) :
    ZMod N)
  0
Tactic: rw [SL2_inv_expl a]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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
have simp : Eq (α := ZMod N) (↑((↑a : 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 *
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N : ℕ
A : ↥(Gamma0 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
Goal:
N : ℕ
A : ↥(Gamma0 N)
ha : 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
have adet : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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) : 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
have 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
Tactic: rw [Matrix.det_fin_two] at adet
Cleared hypotheses: adet
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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) ℤ) 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
have ha₁ : 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 *
Cleared hypotheses: ha, adet
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
⊢ 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
have 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
Tactic: simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul] at *
Cleared hypotheses: ha, adet
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ A ∈ Gamma1' N
have mpr : Eq (α := ZMod N)
  (({ toFun := fun (g : ↥(Gamma0 N)) ↦ (↑((↑(↑g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N),
          map_one' := sorry } :
        (a : ↥(Gamma0 N)) → ZMod N)
      A :
    ZMod N)
  (1 : ZMod N)
Tactic: simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N : ℕ
A : SL(2, ℤ)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
Goal:
N : ℕ
A : SL(2, ℤ)
ha : 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
have ha₁ : ∃ (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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨⟨x, hx⟩, hxx⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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) (↑((↑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
have 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
Tactic: rw [Gamma1_to_Gamma0_mem] at hx
Cleared hypotheses: hxx