∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β}
  {g : C(↑s, β)} (hf : ContinuousOn f s),
  ContinuousMap.mkD (s.restrict f) g = { toFun := s.restrict f, continuous_toFun := ⋯ }