awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
h :
  x ∈ 𝒢 ↔
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        (((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g)⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
      𝒢
h₁ :
  x ∈ 𝒢 ↔
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
      𝒢
h₂ : x ∈ 𝒢 ↔ g⁻¹ * x * g⁻¹⁻¹ ∈ 𝒢
h₃ : x ∈ 𝒢 ↔ g⁻¹ * x * g ∈ 𝒢
h₄ : x ∈ 𝒢 ↔ g⁻¹ * x ∈ 𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have h₅ : x ∈ 𝒢 ↔ x ∈ 𝒢
Tactic: rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← ConjAct.toConjAct_inv,
    ConjAct.toConjAct_smul, inv_inv, Subgroup.mul_mem_cancel_right _ hg,
    Subgroup.mul_mem_cancel_left _ (inv_mem hg)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
⊢ IsCusp c 𝒢' ↔ IsCusp c 𝒢
have refine : IsCusp c 𝒢 → ∀ (g : GL (Fin 2) ℝ) (hg : g ∈ 𝒢) (hgp : g.IsParabolic) (hgc : g • c = c), IsCusp c 𝒢'
Tactic: refine ⟨fun ⟨g, hg, hgp, hgc⟩ ↦ ⟨g, h𝒢 hg, hgp, hgc⟩, fun ⟨g, hg, hgp, hgc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
⊢ IsCusp c 𝒢'
have obtain : ∀ (n : ℕ) (hn : 0 < n) (hgn : g ^ n ∈ 𝒢' ⊓ 𝒢), IsCusp c 𝒢'
Tactic: obtain ⟨n, hn, -, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero h𝒢' hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ IsCusp c 𝒢'
have refine : g ^ n • c = c
Tactic: refine ⟨g ^ n, (Subgroup.mem_inf.mpr hgn).1, hgp.pow hn.ne', ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c
have hn₁ : n ≠ 0
Tactic: rw [Nat.pos_iff_ne_zero] at hn
Cleared hypotheses: hn, hgn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c
have rwa : c = (g ^ n).parabolicFixedPoint
Tactic: rwa [(hgp.pow hn).smul_eq_self_iff, hgp.parabolicFixedPoint_pow hn, ← hgp.smul_eq_self_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
rwa : c = (g ^ n).parabolicFixedPoint
⊢ g ^ n • c = c
have rwa₁ : c = g.parabolicFixedPoint
Tactic: rwa [(hgp.pow hn).smul_eq_self_iff, hgp.parabolicFixedPoint_pow hn, ← hgp.smul_eq_self_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ IsCusp c 𝒢 ↔ IsCusp c 𝒢'
have h𝒢' : (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0
Tactic: rw [← isCusp_iff_of_relIndex_ne_zero inf_le_left, isCusp_iff_of_relIndex_ne_zero inf_le_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
h𝒢' : (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0
⊢ IsCusp c 𝒢 ↔ IsCusp c 𝒢'
have h𝒢'₁ : (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0
Tactic: rw [← isCusp_iff_of_relIndex_ne_zero inf_le_left, isCusp_iff_of_relIndex_ne_zero inf_le_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
⊢ IsCusp c 𝒢
have hGH : 𝒢.relIndex ℋ ≠ 0
Tactic: have hGH : 𝒢.relIndex ℋ ≠ 0 := 𝒢.relIndex_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : 𝒢.relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
have hGH₁ : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
Tactic: rw [← Subgroup.inf_relIndex_right] at hGH
Cleared hypotheses: hGH
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (hypothesis)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
have hc₁ : IsCusp c (𝒢 ⊓ ℋ)
Tactic: rw [← isCusp_iff_of_relIndex_ne_zero inf_le_right hGH] at hc
Cleared hypotheses: hc, hGH
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢)
have suffices : (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢).IsFiniteRelIndex
  ℋ
Tactic: suffices (ConjAct.toConjAct h • 𝒢).IsFiniteRelIndex ℋ from hc.of_isFiniteRelIndex
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ))
        𝒢).IsFiniteRelIndex
    ℋ
have relIndex_ne_zero : (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢).relIndex
    ℋ ≠
  0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
          ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢).relIndex
      ℋ ≠
    0
have relIndex_ne_zero : 𝒢.relIndex ℋ ≠ 0
Tactic: rw [← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh), 𝒢.relIndex_pointwise_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ↔
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
have mp : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) →
  Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
mp :
  IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) →
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ↔
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
have mpr : Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c →
  IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℚ
⊢ IsCusp (OnePoint.map Rat.cast c) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
have mpr : ∀ (a : SL(2, ℤ)),
  IsCusp
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞))
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
Tactic: obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
a : SL(2, ℤ)
⊢ IsCusp
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞))
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
have mpr : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))
Tactic: refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
a : SL(2, ℤ)
mpr : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))
⊢ IsCusp
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞))
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
have mpr₁ : HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
    ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹) : GL (Fin 2) ℝ)
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞)) =
  OnePoint.map Rat.cast
    (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ) ∞)
Tactic: refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
a : SL(2, ℤ)
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))
have mpr : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T)
Tactic: suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
a : SL(2, ℤ)
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T)
have mpr : Eq (α := ℝ)
  (Matrix.discr (n := Fin 2) (↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ)) 0
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
a : SL(2, ℤ)
⊢ Eq (α := ℝ)
    (Matrix.discr (n := Fin 2) (↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ))
    0
have mpr : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2 - 4 = 0
Tactic: simp [discr_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: rw [isCusp_SL2Z_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
⊢ 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) ℝ) ∞
have 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) ℝ) ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
⊢ 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) ℝ) ∞
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℚ
⊢ ∃ (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) ℝ) ∞
have 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) ℝ) ∞
Tactic: obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ) ∞
have 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) ℝ) ∞
Tactic: refine ⟨g, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
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 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) ℝ) ∞
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, ℤ)
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) ℝ) ∞
⊢ 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 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) ℝ) ∞
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, ℤ)
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) ℝ) ∞
⊢ 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 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) ℝ) ∞
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, ℤ)
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) ℝ) ∞
⊢ 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 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) ℝ) ∞
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, ℤ)
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) ℝ) ∞
⊢ 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 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) ℝ) ∞
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, ℤ)
⊢ 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) ℝ) ∞)
have 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) ℝ) ∞
Tactic: refine ⟨mapGL ℚ g • ∞, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
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 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) ℝ) ∞
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) ℝ) ∞
⊢ 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) ℝ)
    (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, g.map_mapGL]