∀ {𝒢 : 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],
  MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (∏ i, SlashInvariantForm.quotientFunc f i)