∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ]
  [SlashInvariantFormClass F Γ k] (f : F) (τ : UpperHalfPlane) {h : ℝ}, h ∈ Γ.strictPeriods → f (h +ᵥ τ) = f τ