awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : 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
⊢ z.det = 1
have rwa₂ : ∀ (this : (↑z.det : ℚ) = HMul.hMul (α := ℚ) (det (n := Fin 2) 1) (↑y.det : ℚ)), z.det = 1
Tactic: rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this
Cleared hypotheses: this
-- 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' : 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
⊢ z.det = 1
have rwa₃ : ∀ (this : (↑z.det : ℚ) = HMul.hMul (α := ℚ) 1 (↑y.det : ℚ)), z.det = 1
Tactic: rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this
Cleared hypotheses: this
-- 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' : 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
⊢ z.det = 1
have rwa₄ : ∀ (this : Eq (α := ℚ) (↑z.det : ℚ) (↑y.det : ℚ)), z.det = 1
Tactic: rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this
Cleared hypotheses: this
-- 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' : 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
⊢ z.det = 1
have rwa₅ : ∀ (this : Eq (α := ℚ) (↑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
Cleared hypotheses: this
-- 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' : 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
⊢ z.det = 1
have rwa₆ : ∀ (this : 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
Cleared hypotheses: this
-- 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) ℤ
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₂
⊢ 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⁻¹)
have hz_det : 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
-- 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' : 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
⊢ 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⁻¹)
have refine : Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det ∈ (↑Γ(M) : Set SL(2, ℤ))
Tactic: refine ⟨⟨z, hz_det⟩, ?_, by simpa only [Subtype.ext_iff, Subgroup.coe_mul, Units.ext_iff,
    Units.val_mul] using hz_coe⟩
-- 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' : 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
⊢ Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) z hz_det ∈ (↑Γ(M) : Set SL(2, ℤ))
have 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))
Tactic: rw [SetLike.mem_coe, CongruenceSubgroup.Gamma_mem', Subtype.ext_iff]
-- 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' : 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
⊢ 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))
have 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)
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' : 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
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)
have a : Eq (α := ZMod M)
  ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z i
      j :
    ZMod M)
  ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_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' : 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
i j : Fin 2
a :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z
        i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₃ :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (1 + M • (A₁.num * k * A₂.num)) i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
⊢ 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)
have a₄ : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M))
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        1 :
      Matrix (Fin 2) (Fin 2) (ZMod M))
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (M • (A₁.num * k * A₂.num)) :
      Matrix (Fin 2) (Fin 2) (ZMod M))
    i j =
  (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_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' : 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
i j : Fin 2
a :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z
        i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₃ :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (1 + M • (A₁.num * k * A₂.num)) i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₄ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          1 :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
⊢ 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)
have a₅ : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (M • (A₁.num * k * A₂.num)) :
      Matrix (Fin 2) (Fin 2) (ZMod M))
    i j =
  (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_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' : 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
i j : Fin 2
a :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z
        i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₃ :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (1 + M • (A₁.num * k * A₂.num)) i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₄ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          1 :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₅ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
⊢ 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)
have a₆ : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
    ((M • (A₁.num * k * A₂.num)).map (⇑(Int.castRingHom (ZMod M)) : (a : ℤ) → ZMod M)) i j =
  (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_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' : 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
i j : Fin 2
a :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M)) z
        i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₃ :
  Eq (α := ZMod M)
    ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
        (1 + M • (A₁.num * k * A₂.num)) i j :
      ZMod M)
    ((↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j : ZMod M)
a₄ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          1 :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₅ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((RingHom.mapMatrix (Int.castRingHom (ZMod M)) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) (ZMod M))
          (M • (A₁.num * k * A₂.num)) :
        Matrix (Fin 2) (Fin 2) (ZMod M))
      i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
a₆ :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
      ((M • (A₁.num * k * A₂.num)).map (⇑(Int.castRingHom (ZMod M)) : (a : ℤ) → ZMod M)) i j =
    (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
⊢ 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)
have a₇ : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) (ZMod M)) (β := Matrix (Fin 2) (Fin 2) (ZMod M)) 1
    ((M • (A₁.num * k * A₂.num)).map fun (x : ℤ) ↦ (↑x : ZMod M)) i j =
  (↑1 : Matrix (Fin 2) (Fin 2) (ZMod M)) i j
Tactic: simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
    Int.cast_natCast, ZMod.natCast_self M, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
M : ℕ
inst : NeZero 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)
have 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)
Tactic: obtain ⟨N, hN, h⟩ := exists_Gamma_le_conj g M