no goals
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
    (forget TopCat).map g ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd
simpa using ConcreteCategory.congr_hom pullback.condition x
case a
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ ↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x) =
    ↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
        property :=
          (_ :
            (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
              (forget TopCat).map g ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (forget TopCat).map (pullbackIsoProdSubtype f g).hom x =
    { val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
      property :=
        (_ :
          (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
            (forget TopCat).map g ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }
apply Subtype.ext
case a.h₁
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x)).fst =
    (↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
          property :=
            (_ :
              (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
                (forget TopCat).map g
                  ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }).fst

case a.h₂
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x)).snd =
    (↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
          property :=
            (_ :
              (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
                (forget TopCat).map g
                  ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }).snd
case a
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ ↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x) =
    ↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
        property :=
          (_ :
            (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
              (forget TopCat).map g ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }
apply Prod.ext
no goals
case a.h₁
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x)).fst =
    (↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
          property :=
            (_ :
              (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
                (forget TopCat).map g
                  ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }).fst

case a.h₂
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ (↑((forget TopCat).map (pullbackIsoProdSubtype f g).hom x)).snd =
    (↑{ val := ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x),
          property :=
            (_ :
              (forget TopCat).map f ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).fst =
                (forget TopCat).map g
                  ((forget TopCat).map pullback.fst x, (forget TopCat).map pullback.snd x).snd) }).snd
exacts [ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_fst f g) x,
  ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_snd f g) x]