case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) ↔
    x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) =
    {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
ext x
case h.mp
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) →
    x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}

case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x} →
    x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd))
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) ↔
    x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
constructor
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd) y ∈
    {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
case h.mp
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd)) →
    x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
rintro ⟨y, rfl⟩
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f) y =
    (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g) y
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd) y ∈
    {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
simp only [← comp_apply, Set.mem_setOf_eq]
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f) y =
    (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g) y
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f) y =
    (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g) y
congr 1
no goals
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f) y =
    (forget TopCat).map (prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g) y
simp [pullback.condition]
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd))
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
⊢ x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x} →
    x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd))
intro h
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd)
      ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h }) =
    x
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ x ∈ Set.range ((forget TopCat).map (prod.lift pullback.fst pullback.snd))
use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
case h.mpr.a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ ∀ (j : Discrete WalkingPair),
    (forget TopCat).map (limit.π (pair X Y) j)
        ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
          ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
      (forget TopCat).map (limit.π (pair X Y) j) x
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (prod.lift pullback.fst pullback.snd)
      ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h }) =
    x
apply Concrete.limit_ext
case h.mpr.a.mk.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left }) x

case h.mpr.a.mk.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right }) x
case h.mpr.a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ ∀ (j : Discrete WalkingPair),
    (forget TopCat).map (limit.π (pair X Y) j)
        ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
          ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
      (forget TopCat).map (limit.π (pair X Y) j) x
rintro ⟨⟨⟩⟩
case h.mpr.a.mk.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ContinuousMap.toFun (limit.π (pair X Y) { as := WalkingPair.left }) x
case h.mpr.a.mk.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left }) x
conv_rhs => rw [hom_apply]
no goals
case h.mpr.a.mk.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.left })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ContinuousMap.toFun (limit.π (pair X Y) { as := WalkingPair.left }) x
simp
case h.mpr.a.mk.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ContinuousMap.toFun (limit.π (pair X Y) { as := WalkingPair.right }) x
case h.mpr.a.mk.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right }) x
conv_rhs => rw [hom_apply]
no goals
case h.mpr.a.mk.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (forget TopCat).obj (X ⨯ Y)
h : x ∈ {x | (forget TopCat).map (prod.fst ≫ f) x = (forget TopCat).map (prod.snd ≫ g) x}
⊢ (forget TopCat).map (limit.π (pair X Y) { as := WalkingPair.right })
      ((forget TopCat).map (prod.lift pullback.fst pullback.snd)
        ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ContinuousMap.toFun (limit.π (pair X Y) { as := WalkingPair.right }) x
simp