awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : 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⁻¹ : GL (Fin 2) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : 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)
have hab₁ : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.comap (mapGL ℝ) 𝒢) (a⁻¹ * b)
Tactic: rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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)
have 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) ℝ) ∞)
          sorry))
    (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) ℝ) ∞)
    sorry)
Tactic: refine Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
g : 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⁻¹ : GL (Fin 2) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]