∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
          Filter.Tendsto f (Filter.comap Complex.im Filter.atTop) (nhds (Function.Periodic.cuspFunction h f 0))