case h₁
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((forget TopCat).map (prodIsoProd X Y).hom x).fst =
    ((forget TopCat).map prod.fst x, (forget TopCat).map prod.snd x).fst

case h₂
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((forget TopCat).map (prodIsoProd X Y).hom x).snd =
    ((forget TopCat).map prod.fst x, (forget TopCat).map prod.snd x).snd
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ (forget TopCat).map (prodIsoProd X Y).hom x = ((forget TopCat).map prod.fst x, (forget TopCat).map prod.snd x)
apply Prod.ext
no goals
case h₁
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((forget TopCat).map (prodIsoProd X Y).hom x).fst =
    ((forget TopCat).map prod.fst x, (forget TopCat).map prod.snd x).fst
exact ConcreteCategory.congr_hom (prodIsoProd_hom_fst X Y) x
no goals
case h₂
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((forget TopCat).map (prodIsoProd X Y).hom x).snd =
    ((forget TopCat).map prod.fst x, (forget TopCat).map prod.snd x).snd
exact ConcreteCategory.congr_hom (prodIsoProd_hom_snd X Y) x