awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)

Tactic:
(GeneralLinearGroup.isParabolic_iff_of_upperTriangular rfl).mpr ⟨rfl, hh.ne'⟩

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular, LT.lt.ne', And.intro, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)

Tactic:
exact (GeneralLinearGroup.isParabolic_iff_of_upperTriangular rfl).mpr ⟨rfl, hh.ne'⟩

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular, And.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
⊢ DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods

Tactic:
have : DiscreteTopology 𝒢.adjoinNegOne.strictPeriods := ‹_›
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
inst_1 : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
rw : 0 < 𝒢.adjoinNegOne.strictWidthInfty ↔ IsCusp ∞ 𝒢
rw₁ : IsCusp ∞ 𝒢.adjoinNegOne ↔ IsCusp ∞ 𝒢
rw₂ rw₃ : IsCusp ∞ 𝒢 ↔ IsCusp ∞ 𝒢
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢

Tactic:
rw [widthInfty, strictWidthInfty_pos_iff, (commensurable_adjoinNegOne_self 𝒢).isCusp_iff]

Premises used: Subgroup.commensurable_adjoinNegOne_self, Subgroup.Commensurable.isCusp_iff, Subgroup.widthInfty, Subgroup.strictWidthInfty_pos_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
⊢ 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
⟨fun h ↦ h ▸ widthInfty_mem_periods 𝒢, fun h ↦ ?_⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, Subgroup.widthInfty_mem_periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
refine : ∀ (h : 𝒢.widthInfty ∈ 𝒢.strictPeriods), 𝒢.IsRegularAtInfty
⊢ 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
refine ⟨fun h ↦ h ▸ widthInfty_mem_periods 𝒢, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
apply : 𝒢.periods ≤ 𝒢.strictPeriods
⊢ 𝒢.IsRegularAtInfty

Tactic:
apply 𝒢.strictPeriods_le_periods.antisymm

Premises used: LE.le.antisymm, Subgroup.strictPeriods_le_periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
rwa : AddSubgroup.zmultiples 𝒢.widthInfty ≤ 𝒢.strictPeriods
rwa₁ rwa₂ rwa₃ rwa₄ : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.periods ≤ 𝒢.strictPeriods

Tactic:
rwa [periods_eq_zmultiples_widthInfty, AddSubgroup.zmultiples_le]

Premises used: AddSubgroup.zmultiples_le, Subgroup.periods_eq_zmultiples_widthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ 0 < 𝒢.widthInfty

Tactic:
apply strictWidthInfty_pos

Premises used: Subgroup.strictWidthInfty_pos
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
⊢ ModularGroup.T ∈ Gamma0 N

Tactic:
simp [ModularGroup.T]

Premises used: ModularGroup.T
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
⊢ ModularGroup.T ∈ Gamma1 N

Tactic:
simp [ModularGroup.T]

Premises used: ModularGroup.T
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
h :
  ∀ (x : ℝ),
    x ∈ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) ↔
      Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (↑N : ℝ)) x
⊢ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
⊢ AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
⊢ AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))

Tactic:
have : AddSubgroup.zmultiples ↑N = .map (Int.castAddHom ℝ) (.zmultiples N) := by simp
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h :
  (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) ↔
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
⊢ x ∈ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) ↔
    Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (↑N : ℝ)) x

Tactic:
simp only [this, mem_strictPeriods_iff, Subgroup.mem_map, Gamma_mem]

Premises used: Subgroup.mem_strictPeriods_iff, Subgroup.mem_map, CongruenceSubgroup.Gamma_mem
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h :
  (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) →
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h₁ :
  x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ)) →
    ∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
⊢ (∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)) ↔
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
⊢ x = (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ)

Tactic:
simpa using congr_arg (· 0 1) hx.symm

Premises used: congr_arg, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
h : (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))

Tactic:
rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
h : Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑N : ℤ)) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
⊢ (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ℝ) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))

Tactic:
apply AddSubgroup.mem_map_of_mem

Premises used: AddSubgroup.mem_map_of_mem
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
g : SL(2, ℤ)
hx :
  Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hg : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
h : (↑N : ℤ) ∣ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h₁ h₂ h₃ h₄ : Eq (α := ZMod N) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑N : ℤ)) ((↑g : Matrix (Fin 2) (Fin 2) ℤ) 0 1)

Tactic:
rwa [Int.mem_zmultiples_iff, ← ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: Int.mem_zmultiples_iff, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h :
  ∀ (x_1 : ℤ) (h : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) x_1 (↑N : ℤ)) = x),
    ∃ (x_2 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
          ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
              (↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) :
            Matrix (Fin 2) (Fin 2) ℝ)
          ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ)) →
    ∃ (x_1 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_1 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x_1 : GL (Fin 2) ℝ)
          ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)

Tactic:
simp only [AddSubgroup.mem_map, AddSubgroup.mem_zmultiples_iff, existsAndEq, true_and,
      Units.ext_iff, mapGL_coe_matrix, map_apply_coe, forall_exists_index]

Premises used: Units.ext_iff, Matrix.SpecialLinearGroup.map_apply_coe, forall_exists_index, ExistsAndEq.existsAndEq, AddSubgroup.mem_zmultiples_iff, Matrix.SpecialLinearGroup.mapGL_coe_matrix, AddSubgroup.mem_map, true_and
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := ZMod N) (↑((↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
    Eq (α := ZMod N) (↑((↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
      Eq (α := ZMod N) (↑((↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
        Eq (α := ZMod N) (↑((↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1

Tactic:
simp [ModularGroup.coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
h :
  ∀ (a : ℤ) (ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x),
    Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) :
        Matrix (Fin 2) (Fin 2) ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)
⊢ ∀ (x_1 : ℤ) (h : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) x_1 (↑N : ℤ)) = x),
    ∃ (x_2 : SL(2, ℤ)),
      (Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 0) : ZMod N) 1 ∧
          Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 0 1) : ZMod N) 0 ∧
            Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ZMod N) 0 ∧
              Eq (α := ZMod N) (↑((↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ZMod N) 1) ∧
        Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
          ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
              (↑x_2 : Matrix (Fin 2) (Fin 2) ℤ) :
            Matrix (Fin 2) (Fin 2) ℝ)
          ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
refine fun a ha ↦ ⟨ModularGroup.T ^ (a * N), by simp [ModularGroup.coe_T_zpow], ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
h :
  ∀ (i j : Fin 2),
    Eq (α := ℝ)
      ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) i j :
        ℝ)
      ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) i j : ℝ)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) :
      Matrix (Fin 2) (Fin 2) ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
i j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) i j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) i j : ℝ)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
j : Fin 2
h :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
h₁ :
  Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow, ← ha]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow, ← ha]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow, ← ha]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples (↑N : ℝ) = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples (↑N : ℤ))
a : ℤ
ha : (Int.castAddHom ℝ : (a : ℤ) → ℝ) (HSMul.hSMul (β := ℤ) a (↑N : ℤ)) = x
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ (a * (↑N : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow, ← ha]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
inst : NeZero N
⊢ strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)

Tactic:
have hsp := strictPeriods_Gamma N
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
inst : NeZero N
hsp : strictPeriods (Subgroup.map (mapGL ℝ) Γ(N)) = AddSubgroup.zmultiples (↑N : ℝ)
⊢ (↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) ∨ -(↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N))

Tactic:
rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff
      (not_isOfFinAddOrder_of_isAddTorsionFree (NeZero.ne _))] at hsp

Premises used: not_isOfFinAddOrder_of_isAddTorsionFree, Eq.comm, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty, NeZero.ne, AddSubgroup.zmultiples_eq_zmultiples_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
N : ℕ
inst : NeZero N
hsp :
  (↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) ∨ -(↑N : ℝ) = strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N))
⊢ strictWidthInfty (Subgroup.map (mapGL ℝ) Γ(N)) = (↑N : ℝ)

Tactic:
grind [strictWidthInfty_nonneg, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, Subgroup.strictWidthInfty_nonneg