∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (f : F)
  [ModularFormClass F Γ k] (g : GL (Fin 2) ℝ),
  MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (SlashAction.map k g ⇑f)