J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
esto : ↑(pullback f g) ≃ₜ ↑X :=
  Homeomorph.trans
    (Homeomorph.ofEmbedding ((forget TopCat).map pullback.fst) (_ : Embedding ((forget TopCat).map pullback.fst)))
    (Homeomorph.mk
      { toFun := Subtype.val,
        invFun := fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) },
        left_inv :=
          (_ :
            ∀ (x : ↑(Set.range ((forget TopCat).map pullback.fst))),
              (fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) ↑x = x),
        right_inv :=
          (_ :
            ∀ (x : ↑X),
              ↑((fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) x) =
                ↑((fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) x)) })
⊢ IsIso pullback.fst
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
⊢ IsIso pullback.fst
let esto : (pullback f g : TopCat) ≃ₜ X :=
  (Homeomorph.ofEmbedding _ (fst_embedding_of_right_embedding f hg)).trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by
          rw [pullback_fst_range]
          exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩⟩
      left_inv := fun ⟨_, _⟩ => rfl
      right_inv := fun x => rfl }
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
esto : ↑(pullback f g) ≃ₜ ↑X :=
  Homeomorph.trans
    (Homeomorph.ofEmbedding ((forget TopCat).map pullback.fst) (_ : Embedding ((forget TopCat).map pullback.fst)))
    (Homeomorph.mk
      { toFun := Subtype.val,
        invFun := fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) },
        left_inv :=
          (_ :
            ∀ (x : ↑(Set.range ((forget TopCat).map pullback.fst))),
              (fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) ↑x = x),
        right_inv :=
          (_ :
            ∀ (x : ↑X),
              ↑((fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) x) =
                ↑((fun x => { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map pullback.fst)) }) x)) })
⊢ IsIso pullback.fst
convert IsIso.of_iso (isoOfHomeo esto)
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
x : ↑X
⊢ x ∈ {x | ∃ y, (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
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
x : ↑X
⊢ x ∈ Set.range ((forget TopCat).map pullback.fst)
rw [pullback_fst_range]
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ((forget TopCat).map g)
H : Set.range ((forget TopCat).map f) ⊆ Set.range ((forget TopCat).map g)
x : ↑X
⊢ x ∈ {x | ∃ y, (forget TopCat).map f x = (forget TopCat).map g y}
exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩