awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
⊢ 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 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
Tactic: simp only [Subgroup.mem_top, true_and] at hxx
Cleared hypotheses: hxx
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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) (↑((↑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 : 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: rw [← hxx]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
⊢ ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A
have hA : A ∈ Gamma0 N
Tactic: have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
⊢ ∃ (x : ↥(Gamma1' N)),
    Membership.mem (γ := Subgroup ↥(Gamma1' N)) ⊤ x ∧
      ((Gamma0 N).subtype.comp (Gamma1' N).subtype : (a : ↥(Gamma1' N)) → SL(2, ℤ)) x = A
have HA : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
have 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
Tactic: refine ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
have 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
Tactic: simp only [Gamma0_mem, Gamma1_mem] at *
Cleared hypotheses: HA
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K
have obtain : ∀ (N : ℕ) (hN : N ≠ 0 ∧ Γ(N) ≤ H), IsCongruenceSubgroup K
Tactic: obtain ⟨N, hN⟩ := h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
N : ℕ
inst : NeZero N
⊢ IsCongruenceSubgroup (Gamma1 N)
have refine : ∀ (A : SL(2, ℤ)) (hA : A ∈ Γ(N)), A ∈ Gamma1 N
Tactic: refine ⟨N, NeZero.ne _, fun A hA ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ Γ.FiniteIndex
have obtain : ∀ (N : ℕ) (hN : N ≠ 0 ∧ Γ(N) ≤ Γ), Γ.FiniteIndex
Tactic: obtain ⟨N, hN⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ Γ.FiniteIndex
have this : NeZero N
Tactic: have : NeZero N := ⟨hN.1⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g : 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, ℤ)) Γ
have 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, ℤ)) Γ
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g 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, ℤ)) Γ
have h : (∃ y ∈ Γ,
    (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
      HMul.hMul (β := GL (Fin 2) ℝ)
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
            GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
            GL (Fin 2) ℝ))
        (((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
          GL (Fin 2) ℝ)) ↔
  x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
Tactic: simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff,
    exists_eq_right, toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
h :
  (∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ)
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ))
          (((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
            GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct 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, ℤ)) Γ
have h₁ : (∃ y ∈ Γ,
    (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
      HMul.hMul (β := GL (Fin 2) ℝ)
        (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
            GL (Fin 2) ℝ)
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
            GL (Fin 2) ℝ))
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)) ↔
  x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
Tactic: simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff,
    exists_eq_right, toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
h :
  (∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ)
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ))
          (((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))⁻¹ :
            GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
h₁ :
  (∃ y ∈ Γ,
      (toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) =
        HMul.hMul (β := GL (Fin 2) ℝ)
          (HMul.hMul (α := GL (Fin 2) ℝ) (β := GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
              GL (Fin 2) ℝ)
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) x) :
              GL (Fin 2) ℝ))
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
            GL (Fin 2) ℝ)) ↔
    x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct 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, ℤ)) Γ
have h₂ : (∃ y ∈ Γ,
    Eq (α := GL (Fin 2) ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) y) :
        GL (Fin 2) ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (g * x * g⁻¹)) :
        GL (Fin 2) ℝ)) ↔
  x ∈ HSMul.hSMul (α := ConjAct SL(2, ℤ)) ((toConjAct : (a : SL(2, ℤ)) → ConjAct SL(2, ℤ)) g⁻¹ : ConjAct SL(2, ℤ)) Γ
Tactic: simp_rw [mem_conjGL, ← map_inv, ← map_mul, toGL_injective.eq_iff, map_intCast_injective.eq_iff,
    exists_eq_right, toConjAct_inv, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)
have obtain : ∀ (N : ℕ) (HN : N ≠ 0 ∧ Γ(N) ≤ Γ), IsCongruenceSubgroup (g • Γ)
Tactic: obtain ⟨N, HN⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
have refine : N ≠ 0 ∧ Γ(N) ≤ g • Γ
Tactic: refine ⟨N, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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) ℚ)
⊢ ∃ (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⁻¹)
have hA₁₂ : 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₂]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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⁻¹)
have 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⁻¹)
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' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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
have 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)))
Tactic: rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
Cleared hypotheses: hy'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
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) ℤ), y = 1 + (a₁ * a₂ * M) • k
have hy'₁ : 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'
Cleared hypotheses: hy'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ ∃ (k : Matrix (Fin 2) (Fin 2) ℤ), y = 1 + (a₁ * a₂ * M) • k
have 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) ℤ)
Tactic: use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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) ℤ)
have 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) ℤ)
Tactic: rw [← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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
⊢ 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) ℤ)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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 =
    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
have 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 : ℤ)))
Tactic: simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
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 : ℤ)))
have h : HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j
Tactic: refine (Int.mul_ediv_cancel_of_dvd ?_).symm