J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ (pullback f g).str =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
let homeo := homeoOfIso (pullbackIsoProdSubtype f g)
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (topologicalSpace_coe (of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd })) =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ (pullback f g).str =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
refine' homeo.inducing.induced.trans _
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (topologicalSpace_coe (of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd })) =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
change induced homeo (induced _ ( (induced Prod.fst X.str) ⊓ (induced Prod.snd Y.str))) = _
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) X.str ⊓
      induced ((Prod.snd ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) Y.str =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
simp only [induced_compose, induced_inf]
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (forget TopCat).map f p.fst = (forget TopCat).map g p.snd }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) X.str ⊓
      induced ((Prod.snd ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) Y.str =
    induced ((forget TopCat).map pullback.fst) X.str ⊓ induced ((forget TopCat).map pullback.snd) Y.str
congr