no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.260169
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : OpenEmbedding g
⊢ OpenEmbedding (g ∘ f) ↔ OpenEmbedding f
simp only [openEmbedding_iff_continuous_injective_open, ← hg.isOpenMap_iff, ←
  hg.1.continuous_iff, hg.inj.of_comp_iff]