∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X]
  (f : X → Y) (y : Y),
  Filter.Tendsto f Filter.cofinite (nhds y) →
    Filter.Tendsto (⇑{ toFun := f, continuous_toFun := ⋯ }) (Filter.coclosedCompact X) (nhds y)