[GOAL]
X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (compHausToTop ⋙ topToLocale).map a₁✝ = (compHausToTop ⋙ topToLocale).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
dsimp at h 
[GOAL]
X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (Opens.comap a₁✝).op = (Opens.comap a₂✝).op
⊢ a₁✝ = a₂✝
[PROOFSTEP]
exact Opens.comap_injective (Quiver.Hom.op_inj h)
