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' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) (y.map Int.cast) 1
i j : Fin 2
⊢ HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j
have h : ∀ (hy' : Eq (α := Matrix (Fin 2) (Fin 2) (ZMod (a₁ * a₂ * M))) ((y - 1).map Int.cast) 0) (i j : Fin 2),
  HMul.hMul (α := ℤ) (↑a₁ : ℤ) (↑a₂ : ℤ) * (↑M : ℤ) ∣ HSub.hSub (β := Matrix (Fin 2) (Fin 2) ℤ) y 1 i j
Tactic: rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'
Cleared hypotheses: hy', 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)
⊢ 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 obtain : ∀ (k : Matrix (Fin 2) (Fin 2) ℤ) (hk : y = 1 + (a₁ * a₂ * M) • k),
  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: obtain ⟨k, hk⟩ : ∃ k, y = 1 + (a₁ * a₂ * M) • k := by
    replace hy' : y.map (Int.cast : ℤ → ZMod (a₁ * a₂ * M)) = 1 := by
      rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
      simpa using hy'
    use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)
    rw [← sub_eq_iff_eq_add']
    ext i j
    simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]
    refine (Int.mul_ediv_cancel_of_dvd ?_).symm
    rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'
    simpa only [Matrix.zero_apply, Matrix.map_apply, ZMod.intCast_zmod_eq_zero_iff_dvd,
      Nat.cast_mul] using congr_fun₂ hy' 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)
⊢ z.map Int.cast = A₁ * y.map Int.cast * A₂
have simp : (M • (A₁.num * k * A₂.num)).map Int.cast = A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂
Tactic: simp only [Matrix.map_add _ Int.cast_add, Matrix.map_one _ Int.cast_zero Int.cast_one, hk,
      mul_add, mul_one, add_mul, hA₁₂, add_right_inj, z]
-- 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)
| A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂
have rw : HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
    HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
  HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)
Tactic: rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]
-- 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)
⊢ (M • (A₁.num * k * A₂.num)).map Int.cast = A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂
have conv_rhs : (M • (A₁.num * k * A₂.num)).map Int.cast =
  HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
      HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
    HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)
Tactic: conv_rhs => rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]
-- 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)
⊢ (M • (A₁.num * k * A₂.num)).map Int.cast =
    HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₁.den : ℚ)⁻¹ (A₁.num.map Int.cast) *
        HSMul.hSMul (β := Matrix (Fin 2) (Fin 2) ℚ) (a₁ * a₂ * M) (k.map Int.cast) *
      HSMul.hSMul (α := ℚ) (β := Matrix (Fin 2) (Fin 2) ℚ) (↑A₂.den : ℚ)⁻¹ (A₂.num.map Int.cast)
have simp : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
    ((a₁ * a₂ * M) •
      HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
Tactic: simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]
-- 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)
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
    (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
      (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
rw :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
        (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw₁ : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) •
    HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
rw :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
        (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
rw₁ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) •
      HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw₂ : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
    (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
rw :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
        (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
rw₁ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) •
      HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₂ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw₃ : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₂ * a₁ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
    (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
rw :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      (HSMul.hSMul (α := ℚ) (↑(a₁ * a₂ * M) : ℚ)
        (HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)))
rw₁ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) •
      HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₂ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₁ * a₂ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
rw₃ :
  M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    (HMul.hMul (α := ℚ) (↑A₂.den : ℚ)⁻¹ (↑(a₂ * a₁ * M) : ℚ) * (↑A₁.den : ℚ)⁻¹) •
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
⊢ M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
    HSMul.hSMul (α := ℚ) (↑A₂.den : ℚ)⁻¹
      ((a₁ * a₂ * M) •
        HSMul.hSMul (α := ℚ) (↑A₁.den : ℚ)⁻¹
          (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast))
have rw₄ : M • (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast) =
  ((↑A₂.den : ℚ)⁻¹ * HMul.hMul (α := ℚ) (↑(a₂ * a₁) : ℚ) (↑M : ℚ) * (↑A₁.den : ℚ)⁻¹) •
    (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℚ) (A₁.num.map Int.cast) (k.map Int.cast) * A₂.num.map Int.cast)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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)
⊢ 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_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
Tactic: have hz_coe : z.map Int.cast = A₁ * (y.map Int.cast) * A₂ := by
    simp only [Matrix.map_add _ Int.cast_add, Matrix.map_one _ Int.cast_zero Int.cast_one, hk,
      mul_add, mul_one, add_mul, hA₁₂, add_right_inj, z]
    conv_rhs => rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]
    simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]
    rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
-- 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₂
⊢ z.det = 1
have this : det (z.map Int.cast) = (A₁ * y.map Int.cast * A₂).det
Tactic: have := congr_arg Matrix.det hz_coe
-- 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₂
this : det (z.map Int.cast) = (A₁ * y.map Int.cast * A₂).det
⊢ z.det = 1
have this₁ : (↑z.det : ℚ) = A₁.det * (↑y.det : ℚ) * A₂.det
Tactic: simp_rw [Matrix.det_mul, ← Int.cast_det] 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
⊢ z.det = 1
have rwa : ∀ (this : (↑z.det : ℚ) = A₁.det * A₂.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
⊢ z.det = 1
have rwa₁ : ∀ (this : (↑z.det : ℚ) = (A₁ * A₂).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