case h
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : (forget TopCat).obj X
⊢ x ∈ (forget TopCat).map pullback.fst '' ((forget TopCat).map pullback.snd ⁻¹' U) ↔
    x ∈ (forget TopCat).map f ⁻¹' ((forget TopCat).map g '' U)
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
⊢ (forget TopCat).map pullback.fst '' ((forget TopCat).map pullback.snd ⁻¹' U) =
    (forget TopCat).map f ⁻¹' ((forget TopCat).map g '' U)
ext x
case h.mp
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : (forget TopCat).obj X
⊢ x ∈ (forget TopCat).map pullback.fst '' ((forget TopCat).map pullback.snd ⁻¹' U) →
    x ∈ (forget TopCat).map f ⁻¹' ((forget TopCat).map g '' U)

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