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

case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
⊢ y ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y} → y ∈ Set.range ((forget TopCat).map pullback.snd)
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
⊢ y ∈ Set.range ((forget TopCat).map pullback.snd) ↔ y ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y}
constructor
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map pullback.snd x ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y}
case h.mp
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
⊢ y ∈ Set.range ((forget TopCat).map pullback.snd) → y ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y}
rintro ⟨x, rfl⟩
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map f ((forget TopCat).map pullback.fst x) =
    (forget TopCat).map g ((forget TopCat).map pullback.snd x)
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map pullback.snd x ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y}
use (pullback.fst : pullback f g ⟶ _) x
no goals
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj (pullback f g)
⊢ (forget TopCat).map f ((forget TopCat).map pullback.fst x) =
    (forget TopCat).map g ((forget TopCat).map pullback.snd x)
exact ConcreteCategory.congr_hom pullback.condition x
case h.mpr.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
x : ↑X
eq : (forget TopCat).map f x = (forget TopCat).map g y
⊢ y ∈ Set.range ((forget TopCat).map pullback.snd)
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
⊢ y ∈ {y | ∃ x, (forget TopCat).map f x = (forget TopCat).map g y} → y ∈ Set.range ((forget TopCat).map pullback.snd)
rintro ⟨x, eq⟩
case h.mpr.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
x : ↑X
eq : (forget TopCat).map f x = (forget TopCat).map g y
⊢ (forget TopCat).map pullback.snd
      ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (x, y), property := eq }) =
    y
case h.mpr.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
x : ↑X
eq : (forget TopCat).map f x = (forget TopCat).map g y
⊢ y ∈ Set.range ((forget TopCat).map pullback.snd)
use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
no goals
case h.mpr.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : (forget TopCat).obj Y
x : ↑X
eq : (forget TopCat).map f x = (forget TopCat).map g y
⊢ (forget TopCat).map pullback.snd
      ((forget TopCat).map (pullbackIsoProdSubtype f g).inv { val := (x, y), property := eq }) =
    y
simp