J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ (X ⨯ Y).str = induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (X ⨯ Y).str = induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
let homeo := homeoOfIso (prodIsoProd X Y)
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (topologicalSpace_coe (of (↑X × ↑Y))) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ (X ⨯ Y).str = induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
refine' homeo.inducing.induced.trans _
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (induced Prod.fst (topologicalSpace_coe X) ⊓ induced Prod.snd (topologicalSpace_coe Y)) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (topologicalSpace_coe (of (↑X × ↑Y))) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
change induced homeo (_ ⊓ _) = _
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (Prod.fst ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe X) ⊓
      induced (Prod.snd ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe Y) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (induced Prod.fst (topologicalSpace_coe X) ⊓ induced Prod.snd (topologicalSpace_coe Y)) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
simp [induced_compose]
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (Prod.fst ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe X) ⊓
      induced (Prod.snd ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe Y) =
    induced ((forget TopCat).map prod.fst) X.str ⊓ induced ((forget TopCat).map prod.snd) Y.str
rfl