no goals
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99038
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
x : β
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) x)
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h,
  preimage_univ, continuousWithinAt_univ]