no goals
α : Type u_1
β : Type u_2
γ : Type ?u.165904
δ : Type ?u.165907
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
x : α
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x
simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]