no goals
α : Type u_1
β : Type u_2
γ : Type ?u.325537
δ : Type ?u.325540
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
x : α
s : Set α
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton,
  true_and_iff]