awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
rw :
  Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c ↔
    ∃ (g : SL(2, ℤ)),
      c =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ↔
    ∃ (g : SL(2, ℤ)),
      c =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
rw [isCusp_SL2Z_iff]

Premises used: isCusp_SL2Z_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
mp :
  Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c →
    ∃ (g : SL(2, ℤ)),
      c =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mpr :
  (∃ (g : SL(2, ℤ)),
      c =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
          ∞) →
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
⊢ Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c ↔
    ∃ (g : SL(2, ℤ)),
      c =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℚ
mp :
  ∀ (g : SL(2, ℤ)),
    ∃ (g_1 : SL(2, ℤ)),
      OnePoint.map Rat.cast
          (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ)
            ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ) ∞) =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ)
          ∞
⊢ ∃ (g : SL(2, ℤ)),
    OnePoint.map Rat.cast c =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ

Premises used: Int, OnePoint.exists_mem_SL2, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
⊢ ∃ (g_1 : SL(2, ℤ)),
    OnePoint.map Rat.cast
        (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
          ∞) =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞

Tactic:
⟨g, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
mp :
  OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ ∃ (g_1 : SL(2, ℤ)),
    OnePoint.map Rat.cast
        (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
          ∞) =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞

Tactic:
refine ⟨g, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
mp :
  OnePoint.map (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mp₁ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      (OnePoint.map (X := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mp₂ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mp₃ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (algebraMap ℚ ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mp₄ mp₅ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
      ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

Premises used: Matrix.SpecialLinearGroup.map_mapGL, Real, Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, Rat.castHom, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
⊢ Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast))
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)

Tactic:
⟨mapGL ℚ g • ∞, ?_⟩

Premises used: OnePoint.infty, Set.Mem, Rat, setOf, Exists.intro, HSMul.hSMul, Set.range, Matrix.SpecialLinearGroup.mapGL, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
mpr :
  OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast))
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)

Tactic:
refine ⟨mapGL ℚ g • ∞, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
g : SL(2, ℤ)
mpr :
  OnePoint.map (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mpr₁ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      (OnePoint.map (X := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mpr₂ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mpr₃ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (algebraMap ℚ ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mpr₄ mpr₅ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
⊢ OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

Premises used: Matrix.SpecialLinearGroup.map_mapGL, Real, Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, Rat.castHom, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
c : OnePoint ℝ
⊢ IsCusp c 𝒢 ↔ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
is_commensurable.isCusp_iff

Premises used: Subgroup.IsArithmetic.is_commensurable, Subgroup.Commensurable.isCusp_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : SL(2, ℤ)
rw :
  OnePoint.map (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹ : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₁ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      (OnePoint.map (X := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₂ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₃ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (algebraMap ℚ ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₄ rw₅ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
⊢ OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹ : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞

Tactic:
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]

Premises used: Matrix.SpecialLinearGroup.map_mapGL, Real, Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, Rat.castHom, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a ≈ b
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢) (a⁻¹ * b)

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hab

Premises used: Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢) (a⁻¹ * b)
⊢ Eq (α := CuspOrbits 𝒢)
    ((fun (g : SL(2, ℤ)) ↦
        (⟦Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
              (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
                ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞)
              ⋯⟧ :
          Quotient (α := ↥(cuspsSubMulAction 𝒢)) (MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢))))
      a)
    ((fun (g : SL(2, ℤ)) ↦
        (⟦Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
              (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
                ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞)
              ⋯⟧ :
          Quotient (α := ↥(cuspsSubMulAction 𝒢)) (MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢))))
      b)

Tactic:
Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩

Premises used: Iff.mpr, Subtype.mk, Exists.intro, Quotient.eq
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢) (a⁻¹ * b)
refine :
  Eq (α := ↥(cuspsSubMulAction 𝒢))
    ((fun (m : ↥𝒢) ↦
        HSMul.hSMul (β := ↥(cuspsSubMulAction 𝒢)) m
          (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
            (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) b⁻¹ : GL (Fin 2) ℝ) ∞)
            ⋯))
      (Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ 𝒢) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a⁻¹ * b)) hab))
    (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
      (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) a⁻¹ : GL (Fin 2) ℝ)
        ∞)
      ⋯)
⊢ Eq (α := CuspOrbits 𝒢)
    ((fun (g : SL(2, ℤ)) ↦
        (⟦Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
              (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
                ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞)
              ⋯⟧ :
          Quotient (α := ↥(cuspsSubMulAction 𝒢)) (MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢))))
      a)
    ((fun (g : SL(2, ℤ)) ↦
        (⟦Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
              (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
                ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞)
              ⋯⟧ :
          Quotient (α := ↥(cuspsSubMulAction 𝒢)) (MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢))))
      b)

Tactic:
refine Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢) (a⁻¹ * b)
⊢ Eq (α := ↥(cuspsSubMulAction 𝒢))
    ((fun (m : ↥𝒢) ↦
        HSMul.hSMul (β := ↥(cuspsSubMulAction 𝒢)) m
          (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
            (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) b⁻¹ : GL (Fin 2) ℝ) ∞)
            ⋯))
      (Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ 𝒢) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a⁻¹ * b)) hab))
    (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
      (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) a⁻¹ : GL (Fin 2) ℝ)
        ∞)
      ⋯)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : SL(2, ℤ)
rw :
  OnePoint.map (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ)
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹ : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₁ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      (OnePoint.map (X := ℚ) (⇑(Rat.castHom ℝ) : (a : ℚ) → ℝ) ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₂ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₃ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((GeneralLinearGroup.map (algebraMap ℚ ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ)
          ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹) :
        GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
rw₄ rw₅ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞
⊢ OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g⁻¹ : GL (Fin 2) ℚ)
        ∞) =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞

Tactic:
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]

Premises used: Matrix.SpecialLinearGroup.map_mapGL, Real, Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, Rat.castHom, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ cosetToCuspOrbit 𝒢 ⟦g⟧ =
    ⟦Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g⁻¹ : GL (Fin 2) ℝ) ∞)
        ⋯⟧

Tactic:
rfl

Premises used: cosetToCuspOrbit, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
c : OnePoint ℝ
hc : IsCusp c 𝒢
⊢ ∃ (g : SL(2, ℤ)),
    c = HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'] at hc

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
c : OnePoint ℝ
hc_1 : IsCusp c 𝒢
hc :
  ∃ (g : SL(2, ℤ)),
    c = HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞
mk :
  ∀ (g : SL(2, ℤ))
    (hc :
      IsCusp
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
          ∞)
        𝒢),
    ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
      cosetToCuspOrbit 𝒢 a =
        Quot.mk
          (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
          (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
            (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
            hc)
⊢ ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢) c hc_1)

Tactic:
obtain ⟨g, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
g : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞) 𝒢
h :
  cosetToCuspOrbit 𝒢 ⟦g⁻¹⟧ =
    Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
      (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
          ∞)
        hc)
⊢ ∃ (a : HasQuotient.Quotient SL(2, ℤ) (B := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢)),
    cosetToCuspOrbit 𝒢 a =
      Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
        (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
          (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞)
          hc)

Tactic:
use ⟦g⁻¹⟧
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
b : CuspOrbits 𝒢
g : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞) 𝒢
⊢ cosetToCuspOrbit 𝒢 ⟦g⁻¹⟧ =
    Quot.mk (⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) : ↥(cuspsSubMulAction 𝒢) → ↥(cuspsSubMulAction 𝒢) → Prop)
      (Subtype.mk (p := fun (x : OnePoint ℝ) ↦ x ∈ cuspsSubMulAction 𝒢)
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ)
          ∞)
        hc)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ Finite (CuspOrbits 𝒢)

Tactic:
.of_surjective _ (surjective_cosetToCuspOrbit 𝒢)

Premises used: surjective_cosetToCuspOrbit, Finite.of_surjective
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
x : R
⊢ x ∈ 𝒢.strictPeriods ↔ Membership.mem (α := GL (Fin 2) R) 𝒢 ((upperRightHom : (a : R) → GL (Fin 2) R) x : GL (Fin 2) R)

Tactic:
simp [strictPeriods]

Premises used: Subgroup.strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
k : R
⊢ Membership.mem (γ := AddSubgroup R)
      (AddSubgroup.comap (AddChar.toAddMonoidHom upperRightHom)
        ((toAddSubgroup : (a : Subgroup (GL (Fin 2) R)) → AddSubgroup (Additive (GL (Fin 2) R))) 𝒢))
      k →
    Membership.mem (γ := AddSubgroup R)
      (AddSubgroup.comap (AddChar.toAddMonoidHom upperRightHom)
        ((toAddSubgroup : (a : Subgroup (GL (Fin 2) R)) → AddSubgroup (Additive (GL (Fin 2) R))) 𝒢.adjoinNegOne))
      k

Tactic:
apply 𝒢.le_adjoinNegOne

Premises used: Subgroup.le_adjoinNegOne
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.IsRegularAtInfty
⊢ 𝒢.strictPeriods = 𝒢.periods

Tactic:
h

Premises used: Subgroup.IsRegularAtInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
pos :
  ∀ (h : 𝒢.strictPeriods = 𝒢.periods), 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
neg :
  ∀ (h : ¬𝒢.strictPeriods = 𝒢.periods), 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
by_cases h : 𝒢.strictPeriods = 𝒢.periods

Premises used: Subgroup.strictPeriods, Subgroup.periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
R : Type u_1
inst : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : ¬𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods < 𝒢.periods

Tactic:
replace h := 𝒢.strictPeriods_le_periods.lt_of_ne h