no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ topologicalSpace_forget (pullback f g) =
    induced ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) (topologicalSpace_forget (X ⨯ Y))
simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]