feat(NumberTheory/ModularForms): cusp form submodule of modular forms (leanprover-community#37978)

Introduces the inclusion of cusp forms into modular forms and the corresponding submodule and `IsCuspForm` predicate.

This is in preparation for proving the dimension formula in level one which is in leanprover-community#37979 and see also leanprover-community#37789

The work was done as part of the Sphere packing project. The original code was written by me but the PR was done with the help of Claude Code.

Author: CBirkbeck

Mathlib.lean

@@ -5614,6 +5614,7 @@ public import Mathlib.NumberTheory.ModularForms.Basic
 public import Mathlib.NumberTheory.ModularForms.BoundedAtCusp
 public import Mathlib.NumberTheory.ModularForms.Bounds
 public import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+public import Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
 public import Mathlib.NumberTheory.ModularForms.Cusps
 public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.Delta

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -108,7 +108,7 @@ instance (priority := 100) ModularForm.funLike :
   coe f := f.toFun
   coe_injective' f g h := by cases f; cases g; congr; exact DFunLike.ext' h
 
-instance (priority := 100) ModularFormClass.modularForm :
+instance (priority := 100) ModularForm.instModularFormClass :
     ModularFormClass (ModularForm Γ k) Γ k where
   slash_action_eq f := f.slash_action_eq'
   holo := ModularForm.holo'
@@ -135,6 +135,19 @@ initialize_simps_projections CuspForm (toFun → coe, as_prefix coe)
 
 variable {F Γ k}
 
+/-- Build a `ModularForm Γ k` from any element of a type carrying a `ModularFormClass Γ k`
+instance. -/
+@[simps -fullyApplied]
+def ModularFormClass.modularForm [FunLike F ℍ ℂ] [ModularFormClass F Γ k] (f : F) :
+    ModularForm Γ k where
+  toFun := f
+  slash_action_eq' := SlashInvariantFormClass.slash_action_eq f
+  holo' := ModularFormClass.holo f
+  bdd_at_cusps' := ModularFormClass.bdd_at_cusps f
+
+instance [FunLike F ℍ ℂ] [ModularFormClass F Γ k] : CoeTC F (ModularForm Γ k) :=
+  ⟨ModularFormClass.modularForm⟩
+
 theorem ModularForm.toFun_eq_coe (f : ModularForm Γ k) : f.toFun = (f : ℍ → ℂ) :=
   rfl
 
@@ -156,20 +169,23 @@ theorem ModularForm.ext {f g : ModularForm Γ k} (h : ∀ x, f x = g x) : f = g
 theorem CuspForm.ext {f g : CuspForm Γ k} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
-/-- Copy of a `ModularForm` with a new `toFun` equal to the old one. Useful to fix
-definitional equalities. -/
-protected def ModularForm.copy (f : ModularForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) :
-    ModularForm Γ k where
-  toSlashInvariantForm := f.1.copy f' h
+/-- Copy of a `ModularForm` with a new `toFun` equal to the old one, optionally transporting
+along an equality of subgroups. Useful to fix definitional equalities. -/
+protected def ModularForm.copy {Γ' : Subgroup (GL (Fin 2) ℝ)} (f : ModularForm Γ k) (f' : ℍ → ℂ)
+    (h : f' = ⇑f) (hΓ : Γ' = Γ := by rfl) : ModularForm Γ' k where
+  toFun := f'
+  slash_action_eq' A hA := h.symm ▸ f.slash_action_eq' A (hΓ ▸ hA)
   holo' := h.symm ▸ f.holo'
-  bdd_at_cusps' A := h.symm ▸ f.bdd_at_cusps' A
-
-/-- Copy of a `CuspForm` with a new `toFun` equal to the old one. Useful to fix
-definitional equalities. -/
-protected def CuspForm.copy (f : CuspForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) : CuspForm Γ k where
-  toSlashInvariantForm := f.1.copy f' h
+  bdd_at_cusps' hc := h.symm ▸ f.bdd_at_cusps' (hΓ ▸ hc)
+
+/-- Copy of a `CuspForm` with a new `toFun` equal to the old one, optionally transporting
+along an equality of subgroups. Useful to fix definitional equalities. -/
+protected def CuspForm.copy {Γ' : Subgroup (GL (Fin 2) ℝ)} (f : CuspForm Γ k) (f' : ℍ → ℂ)
+    (h : f' = ⇑f) (hΓ : Γ' = Γ := by rfl) : CuspForm Γ' k where
+  toFun := f'
+  slash_action_eq' A hA := h.symm ▸ f.slash_action_eq' A (hΓ ▸ hA)
   holo' := h.symm ▸ f.holo'
-  zero_at_cusps' A := h.symm ▸ f.zero_at_cusps' A
+  zero_at_cusps' hc := h.symm ▸ f.zero_at_cusps' (hΓ ▸ hc)
 
 end ModularForm
 

Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

@@ -69,6 +69,10 @@ theorem Gamma_one_top : Gamma 1 = ⊤ := by
 lemma mem_Gamma_one (γ : SL(2, ℤ)) : γ ∈ Γ(1) := by
   simp only [Gamma_one_top, Subgroup.mem_top]
 
+/-- The GL-image of `Γ(1)` equals `𝒮ℒ` (the image of `SL(2, ℤ)` in `GL(2, ℝ)`). -/
+theorem Gamma_one_coe_eq_SL : (↑(Gamma 1) : Subgroup (GL (Fin 2) ℝ)) = 𝒮ℒ := by
+  simp [Gamma_one_top, MonoidHom.range_eq_map]
+
 theorem Gamma_zero_bot : Gamma 0 = ⊥ := rfl
 
 lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :

Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+module
+
+public import Mathlib.NumberTheory.ModularForms.QExpansion
+public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
+
+/-!
+# Cusp form submodule and IsCuspForm predicate
+
+This file defines the inclusion of cusp forms into modular forms as a linear map, the cusp form
+submodule of modular forms, and the `IsCuspForm` predicate. It also provides a direct constructor
+`ModularForm.toCuspForm` for building cusp forms from modular forms with vanishing constant
+q-expansion coefficient (for `𝒮ℒ`).
+
+## Main definitions
+
+* `CuspForm.toModularFormₗ`: the inclusion `CuspForm Γ k →ₗ[ℂ] ModularForm Γ k`.
+* `ModularForm.cuspFormSubmodule`: the submodule of `ModularForm Γ k` consisting of cusp forms.
+* `ModularForm.IsCuspForm`: predicate that a modular form lies in the cusp form submodule.
+* `ModularForm.toCuspForm`: builds a `CuspForm 𝒮ℒ k` from a `ModularForm` whose q-expansion
+  has vanishing constant term.
+
+## Main results
+
+* `CuspForm.toModularFormₗ_injective`: the inclusion is injective.
+* `CuspForm.equivCuspFormSubmodule`: `CuspForm Γ k ≃ₗ[ℂ] cuspFormSubmodule Γ k`.
+* `ModularForm.isCuspForm_iff_coeffZero_eq_zero`: for `𝒮ℒ`, `IsCuspForm` is equivalent to the
+  q-expansion having vanishing constant term.
+-/
+
+@[expose] public noncomputable section
+
+open UpperHalfPlane ModularForm Complex SlashInvariantForm SlashInvariantFormClass
+  ModularFormClass MatrixGroups OnePoint Filter Topology
+
+variable {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}
+
+namespace CuspForm
+
+/-- The inclusion of cusp forms into modular forms, as a ℂ-linear map. -/
+def toModularFormₗ [Γ.HasDetOne] : CuspForm Γ k →ₗ[ℂ] ModularForm Γ k where
+  toFun := ModularFormClass.modularForm
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+@[simp]
+lemma toModularFormₗ_apply [Γ.HasDetOne] (f : CuspForm Γ k) (z : ℍ) :
+    (toModularFormₗ f) z = f z := rfl
+
+lemma toModularFormₗ_eq_coe [Γ.HasDetOne] (f : CuspForm Γ k) :
+    toModularFormₗ f = (f : ModularForm Γ k) := rfl
+
+lemma toModularFormₗ_injective [Γ.HasDetOne] :
+    Function.Injective (toModularFormₗ : CuspForm Γ k → ModularForm Γ k) :=
+  fun _ _ h ↦ DFunLike.ext _ _ fun z ↦ DFunLike.congr_fun h z
+
+end CuspForm
+
+namespace ModularForm
+
+/-- The submodule of `ModularForm Γ k` consisting of cusp forms, defined as the range of
+the inclusion `CuspForm.toModularFormₗ`. -/
+def cuspFormSubmodule (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) [Γ.HasDetOne] :
+    Submodule ℂ (ModularForm Γ k) :=
+  LinearMap.range CuspForm.toModularFormₗ
+
+/-- A modular form is a cusp form if it lies in the cusp form submodule. -/
+def IsCuspForm [Γ.HasDetOne] (f : ModularForm Γ k) : Prop :=
+  f ∈ cuspFormSubmodule Γ k
+
+@[simp]
+lemma mem_cuspFormSubmodule_iff [Γ.HasDetOne] {f : ModularForm Γ k} :
+    f ∈ cuspFormSubmodule Γ k ↔ IsCuspForm f := Iff.rfl
+
+/-- The cusp form submodule is linearly equivalent to the type of cusp forms. -/
+def CuspForm.equivCuspFormSubmodule (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) [Γ.HasDetOne] :
+    CuspForm Γ k ≃ₗ[ℂ] cuspFormSubmodule Γ k :=
+  LinearEquiv.ofInjective CuspForm.toModularFormₗ CuspForm.toModularFormₗ_injective
+
+/-- A modular form is a cusp form if and only if it vanishes at every cusp. This is the
+general characterization valid for any subgroup. -/
+lemma isCuspForm_iff [Γ.HasDetOne] (f : ModularForm Γ k) :
+    IsCuspForm f ↔ ∀ {c}, IsCusp c Γ → c.IsZeroAt f k :=
+  ⟨fun ⟨g, hg⟩ _ ↦ hg ▸ g.zero_at_cusps', fun h ↦ ⟨⟨f, f.holo', h⟩, rfl⟩⟩
+
+/-- A modular form with `valueAtInfty f = 0` is zero at infinity. -/
+lemma isZeroAtImInfty_of_valueAtInfty_eq_zero {F : Type*} [FunLike F ℍ ℂ]
+    [DiscreteTopology Γ] [Γ.HasDetPlusMinusOne] [Fact (IsCusp ∞ Γ)] [ModularFormClass F Γ k]
+    (f : F) (h : valueAtInfty f = 0) : IsZeroAtImInfty f := by
+  have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
+  have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
+  have hanal := ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
+  have hper := periodic_comp_ofComplex f hΓ
+  simp_rw [IsZeroAtImInfty, ZeroAtFilter, ← h, ← cuspFunction_apply_zero hh hanal hper]
+  exact (hanal.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)).congr
+    (fun τ ↦ SlashInvariantFormClass.eq_cuspFunction f τ hΓ hh.ne')
+
+section SL2Z
+
+open EisensteinSeries
+
+variable {k : ℤ}
+
+/-- An `𝒮ℒ` modular form with vanishing q-expansion constant term vanishes at every cusp. -/
+lemma isZeroAt_of_coeffZero_eq_zero (f : ModularForm 𝒮ℒ k)
+    (h : (qExpansion 1 f).coeff 0 = 0) {c : OnePoint ℝ} (hc : IsCusp c 𝒮ℒ) :
+    c.IsZeroAt f k := by
+  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
+  rw [isZeroAt_iff_forall_SL2Z hc]
+  intro γ _
+  rw [show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩]
+  exact isZeroAtImInfty_of_valueAtInfty_eq_zero f <| by
+    rwa [← qExpansion_coeff_zero one_pos
+      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
+      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)]
+
+/-- Build a `CuspForm 𝒮ℒ k` from a `ModularForm 𝒮ℒ k` whose q-expansion has vanishing
+constant term. The resulting cusp form has the same underlying function. -/
+def toCuspForm (f : ModularForm 𝒮ℒ k) (h : (qExpansion 1 f).coeff 0 = 0) : CuspForm 𝒮ℒ k :=
+  { f with zero_at_cusps' := isZeroAt_of_coeffZero_eq_zero f h }
+
+@[simp]
+lemma toCuspForm_apply (f : ModularForm 𝒮ℒ k) (h : (qExpansion 1 f).coeff 0 = 0)
+    (z : ℍ) : (toCuspForm f h) z = f z := rfl
+
+/-- For `𝒮ℒ` modular forms, `IsCuspForm` is equivalent to the q-expansion having vanishing
+constant term. -/
+lemma isCuspForm_iff_coeffZero_eq_zero (f : ModularForm 𝒮ℒ k) :
+    IsCuspForm f ↔ (qExpansion 1 f).coeff 0 = 0 := by
+  refine ⟨fun ⟨g, hg⟩ ↦ ?_, fun h ↦ (isCuspForm_iff f).mpr (isZeroAt_of_coeffZero_eq_zero f h)⟩
+  rw [← hg, qExpansion_coeff_zero one_pos
+    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
+    (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)]
+  exact (CuspFormClass.zero_at_infty g).valueAtInfty_eq_zero
+
+end SL2Z
+
+end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -327,7 +327,7 @@ lemma EisensteinSeries.E_qExpansion_coeff {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k
   set β : ℂ := -(2 * k / bernoulli k : ℂ)
   set c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑(σ (k - 1) m)
   suffices ∀ τ : ℍ, HasSum (fun m ↦ c m • 𝕢 (1 : ℝ) τ ^ m) (E hk τ) from
-    (ModularFormClass.qExpansion_coeff_unique one_pos one_mem_strictPeriods_SL2Z this m).symm
+    (ModularFormClass.qExpansion_coeff_unique one_pos (by simp) this m).symm
   intro τ
   have hS : Summable fun n : ℕ ↦ (σ (k - 1) (n + 1) : ℂ) * cexp (2 * π * I * τ) ^ (n + 1) :=
     (summable_nat_add_iff 1).mpr (summable_sigma_mul_cexp_pow (by omega) τ)

Mathlib/NumberTheory/ModularForms/LevelOne.lean

@@ -30,19 +30,22 @@ variable {F : Type*} [FunLike F ℍ ℂ] {k : ℤ}
 
 namespace SlashInvariantForm
 
-variable [SlashInvariantFormClass F Γ(1) k]
+variable [SlashInvariantFormClass F 𝒮ℒ k]
 
 lemma exists_one_half_le_im_and_norm_le (hk : k ≤ 0) (f : F) (τ : ℍ) :
     ∃ ξ : ℍ, 1 / 2 ≤ ξ.im ∧ ‖f τ‖ ≤ ‖f ξ‖ :=
   let ⟨γ, hγ, hdenom⟩ := exists_one_half_le_im_smul_and_norm_denom_le τ
-  ⟨γ • τ, hγ, by simpa only [slash_action_eqn_SL'' _ (mem_Gamma_one γ),
-    norm_mul, norm_zpow] using le_mul_of_one_le_left (norm_nonneg _) <|
-      one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk⟩
+  ⟨γ • τ, hγ, by
+    have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
+    simpa only [slash_action_eqn_SL'' _ (mem_Gamma_one γ), norm_mul, norm_zpow]
+      using le_mul_of_one_le_left (norm_nonneg _) <|
+        one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk⟩
 
 variable (k) in
 /-- If a constant function is modular of weight `k`, then either `k = 0`, or the constant is `0`. -/
 lemma wt_eq_zero_of_eq_const {f : F} {c : ℂ} (hf : ⇑f = Function.const _ c) :
     k = 0 ∨ c = 0 := by
+  have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
   have hI := slash_action_eqn_SL'' f (mem_Gamma_one S) I
   have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ((⟨2, two_pos⟩ : {x : ℝ // 0 < x}) • .I)
   simp_rw [sl_moeb, hf, Function.const, denom_S] at hI h2I2
@@ -63,16 +66,16 @@ theorem slash_action_generators_SL2Z {f : ℍ → ℂ} {k : ℤ}
 
 end SlashInvariantForm
 
-namespace ModularFormClass
+lemma one_mem_strictPeriods_SL : (1 : ℝ) ∈ (𝒮ℒ).strictPeriods := by simp
 
-variable [ModularFormClass F Γ(1) k]
+namespace ModularFormClass
 
-lemma one_mem_strictPeriods_SL2Z : (1 : ℝ) ∈ Γ(1).strictPeriods := by simp
+variable [ModularFormClass F 𝒮ℒ k]
 
 private theorem cuspFunction_eqOn_const_of_nonpos_wt (hk : k ≤ 0) (f : F) :
     Set.EqOn (cuspFunction 1 f) (const ℂ (cuspFunction 1 f 0)) (Metric.ball 0 1) := by
   refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)
-  · exact (ModularFormClass.differentiableAt_cuspFunction f one_pos one_mem_strictPeriods_SL2Z
+  · exact (ModularFormClass.differentiableAt_cuspFunction f one_pos one_mem_strictPeriods_SL
       (mem_ball_zero_iff.mp hq)).differentiableWithinAt
   · simp [pi_pos]
   · simp only [Metric.mem_closedBall, dist_zero_right]
@@ -81,15 +84,15 @@ private theorem cuspFunction_eqOn_const_of_nonpos_wt (hk : k ≤ 0) (f : F) :
     · obtain ⟨ξ, hξ, hξ₂⟩ := exists_one_half_le_im_and_norm_le hk f
         ⟨_, im_invQParam_pos_of_norm_lt_one Real.zero_lt_one (mem_ball_zero_iff.mp hq) hq'⟩
       exact ⟨_, norm_qParam_le_of_one_half_le_im hξ,
-        by simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL2Z
+        by simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
             one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂⟩
 
 private theorem levelOne_nonpos_wt_const (hk : k ≤ 0) (f : F) :
     f = Function.const ℍ (cuspFunction 1 f 0) := by
   ext z
   have hQ : 𝕢 1 z ∈ (Metric.ball 0 1) := by
     simpa using (norm_qParam_lt_iff zero_lt_one 0 z.1).mpr z.2
-  simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL2Z one_ne_zero]
+  simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL one_ne_zero]
     using cuspFunction_eqOn_const_of_nonpos_wt hk f hQ
 
 lemma levelOne_neg_weight_eq_zero (hk : k < 0) (f : F) : ⇑f = 0 := by
@@ -98,18 +101,18 @@ lemma levelOne_neg_weight_eq_zero (hk : k < 0) (f : F) : ⇑f = 0 := by
   · exact (lt_irrefl _ hk).elim
   · rw [hf, hf₀, const_zero]
 
-lemma levelOne_weight_zero_const [ModularFormClass F Γ(1) 0] (f : F) :
+lemma levelOne_weight_zero_const [ModularFormClass F 𝒮ℒ 0] (f : F) :
     ∃ c, ⇑f = Function.const _ c :=
   ⟨_, levelOne_nonpos_wt_const le_rfl f⟩
 
 end ModularFormClass
 
-lemma ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm Γ(1) 0) = 1 := by
+lemma ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm 𝒮ℒ 0) = 1 := by
   refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_
   obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g
   aesop
 
 lemma ModularForm.levelOne_neg_weight_rank_zero (hk : k < 0) :
-    Module.rank ℂ (ModularForm Γ(1) k) = 0 := by
+    Module.rank ℂ (ModularForm 𝒮ℒ k) = 0 := by
   refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩
   simpa [← coe_eq_zero_iff] using levelOne_neg_weight_eq_zero hk f

Mathlib/NumberTheory/ModularForms/NormTrace.lean

@@ -142,20 +142,17 @@ lemma ModularForm.isZero_of_neg_weight [𝒢.IsArithmetic]
     {k : ℤ} (hk : k < 0) (f : ModularForm 𝒢 k) : f = 0 := by
   suffices ModularForm.norm 𝒮ℒ f = 0 by simpa [ModularForm.norm_eq_zero_iff]
   ext
-  -- some friction here because `levelOne_neg_weight_eq_zero` uses `Γ(1)` for the level
-  rw [@ModularFormClass.levelOne_neg_weight_eq_zero (f := ModularForm.norm 𝒮ℒ f) _ _ _,
-    Pi.zero_apply, zero_apply]
-  · rw [CongruenceSubgroup.Gamma_one_top, ← MonoidHom.range_eq_map]
-    infer_instance
-  · exact mul_neg_of_neg_of_pos hk <| mod_cast Nat.pos_of_ne_zero 𝒢.relIndex_ne_zero
+  rw [ModularFormClass.levelOne_neg_weight_eq_zero
+    (mul_neg_of_neg_of_pos hk <| mod_cast Nat.pos_of_ne_zero 𝒢.relIndex_ne_zero)
+    (ModularForm.norm 𝒮ℒ f), Pi.zero_apply, zero_apply]
 
 private lemma ModularForm.eq_const_of_weight_zero₀ [𝒢.IsArithmetic] [𝒢.HasDetOne]
     (f : ModularForm 𝒢 0) : ∃ c, (f : ℍ → ℂ) = Function.const ℍ c := by
   -- Consider the norm of `f - (f I)`. This must be a constant, since it's a weight 0 level 1 form.
-  obtain ⟨c, hc⟩ : ∃ c, (ModularForm.norm 𝒮ℒ (f - .const (f I)) : ℍ → ℂ) = Function.const ℍ c := by
-    convert @ModularFormClass.levelOne_weight_zero_const
-      (f := ModularForm.norm 𝒮ℒ (f - .const (f I))) _ (by infer_instance)
-      (by rw [zero_mul, CongruenceSubgroup.Gamma_one_top, MonoidHom.range_eq_map]; infer_instance)
+  let : ModularFormClass (ModularForm 𝒮ℒ (0 * Nat.card (𝒮ℒ ⧸ 𝒢.subgroupOf 𝒮ℒ))) 𝒮ℒ 0 := by
+    rw [zero_mul]; infer_instance
+  obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
+    (ModularForm.norm 𝒮ℒ (f - .const (f I)))
   -- But the constant must be 0, since `f - f I` vanishes at `I`.
   have : ModularForm.norm 𝒮ℒ (f - .const (f I)) I = 0 := by
     simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩