∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R]
  [inst_3 : TopologicalSpace α] {f : α → R} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => star (f x)) s x