∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (toContinuousMap : C(α, β))
  (cocompact_tendsto' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (Filter.cocompact β))
  (toContinuousMap_1 : C(α, β))
  (cocompact_tendsto'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (Filter.cocompact β)),
  ({ toContinuousMap := toContinuousMap, cocompact_tendsto' := cocompact_tendsto' } =
      { toContinuousMap := toContinuousMap_1, cocompact_tendsto' := cocompact_tendsto'_1 }) =
    (toContinuousMap = toContinuousMap_1)