∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ModularFormClass F 𝒢 k] {c : OnePoint ℝ},
  IsCusp c ℋ →
    ∀ (γ : GL (Fin 2) ℝ),
      γ • OnePoint.infty = c →
        UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ (SlashInvariantForm.trace ℋ f).toFun)