a lemma about --inducing-- open_embedding?

Stream: Is there code for X?

[Scott Morrison]

import topology.local_homeomorph

lemma open_embedding.continuous_at_iff
  {X Y Z : Type*} [topological_space X] [topological_space Y] [topological_space Z]
  {f : X → Y} {g : Y → Z} (hf : open_embedding f) {x : X} :
  continuous_at (g ∘ f) x ↔ continuous_at g (f x) :=
begin
  haveI : nonempty X := ⟨x⟩,
  convert ((hf.to_local_homeomorph.continuous_at_iff_continuous_at_comp_right) _).symm,
  { apply (local_homeomorph.left_inv _ _).symm,
    simp, },
  { simp, },
end