[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous (Prod.fst ∘ Subtype.val)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case hg
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous Prod.fst
[PROOFSTEP]
continuity
[GOAL]
case hf
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous Subtype.val
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous (Prod.snd ∘ Subtype.val)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case hg
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous Prod.snd
[PROOFSTEP]
continuity
[GOAL]
case hf
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous Subtype.val
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackFst f g ≫ f = pullbackSnd f g ≫ g
[PROOFSTEP]
dsimp [pullbackFst, pullbackSnd, Function.comp]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (ContinuousMap.mk fun x => (↑x).fst) ≫ f = (ContinuousMap.mk fun x => (↑x).snd) ≫ g
[PROOFSTEP]
ext ⟨x, h⟩
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑X × ↑Y
h : ↑f x.fst = ↑g x.snd
⊢ ↑((ContinuousMap.mk fun x => (↑x).fst) ≫ f) { val := x, property := h } =
    ↑((ContinuousMap.mk fun x => (↑x).snd) ≫ g) { val := x, property := h }
[PROOFSTEP]
rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk]
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑X × ↑Y
h : ↑f x.fst = ↑g x.snd
⊢ ↑f (↑{ val := x, property := h }).fst = ↑g (↑{ val := x, property := h }).snd
[PROOFSTEP]
exact h
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst s ∧
        l ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd s ∧
          ∀ {m : s.pt ⟶ (pullbackCone f g).pt},
            m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst s →
              m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd s → m = l }
[PROOFSTEP]
intro S
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ { l //
    l ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S ∧
      l ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S ∧
        ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
          m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S →
            m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S → m = l }
[PROOFSTEP]
constructor
[GOAL]
case property
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ?val ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S ∧
    ?val ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S →
          m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S → m = ?val
case val
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt
[PROOFSTEP]
swap
[GOAL]
case val
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt
case property
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ?val ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S ∧
    ?val ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S →
          m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S → m = ?val
[PROOFSTEP]
exact
  { toFun := fun x => ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩
    continuous_toFun := by
      apply Continuous.subtype_mk <| Continuous.prod_mk ?_ ?_
      · exact (PullbackCone.fst S) |>.continuous_toFun
      · exact (PullbackCone.snd S) |>.continuous_toFun }
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
x : ↑S.pt
⊢ ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst = ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd
[PROOFSTEP]
simpa using ConcreteCategory.congr_hom S.condition x
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ Continuous fun x =>
    { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
      property :=
        (_ :
          ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
            ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }
[PROOFSTEP]
apply Continuous.subtype_mk <| Continuous.prod_mk ?_ ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ Continuous fun x => ↑(PullbackCone.fst S) x
[PROOFSTEP]
exact (PullbackCone.fst S) |>.continuous_toFun
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ Continuous fun x => ↑(PullbackCone.snd S) x
[PROOFSTEP]
exact (PullbackCone.snd S) |>.continuous_toFun
[GOAL]
case property
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ (ContinuousMap.mk fun x =>
          { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
            property :=
              (_ :
                ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                  ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
        PullbackCone.fst (pullbackCone f g) =
      PullbackCone.fst S ∧
    (ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
          PullbackCone.snd (pullbackCone f g) =
        PullbackCone.snd S ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S →
          m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S →
            m =
              ContinuousMap.mk fun x =>
                { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
                  property :=
                    (_ :
                      ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                        ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case property.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ (ContinuousMap.mk fun x =>
        { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
          property :=
            (_ :
              ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
      PullbackCone.fst (pullbackCone f g) =
    PullbackCone.fst S
[PROOFSTEP]
delta pullbackCone
[GOAL]
case property.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ (ContinuousMap.mk fun x =>
        { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
          property :=
            (_ :
              ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
      PullbackCone.fst
        (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)) =
    PullbackCone.fst S
[PROOFSTEP]
ext a
[GOAL]
case property.refine'_1.w
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (forget TopCat).obj S.pt
⊢ ↑((ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
          PullbackCone.fst
            (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)))
      a =
    ↑(PullbackCone.fst S) a
[PROOFSTEP]
rw [comp_apply, ContinuousMap.coe_mk]
[GOAL]
case property.refine'_1.w
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (forget TopCat).obj S.pt
⊢ ↑(PullbackCone.fst
          (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)))
      { val := (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a),
        property :=
          (_ :
            ↑f (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a).fst =
              ↑g (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a).snd) } =
    ↑(PullbackCone.fst S) a
[PROOFSTEP]
rfl
[GOAL]
case property.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ (ContinuousMap.mk fun x =>
        { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
          property :=
            (_ :
              ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
      PullbackCone.snd (pullbackCone f g) =
    PullbackCone.snd S
[PROOFSTEP]
delta pullbackCone
[GOAL]
case property.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ (ContinuousMap.mk fun x =>
        { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
          property :=
            (_ :
              ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
      PullbackCone.snd
        (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)) =
    PullbackCone.snd S
[PROOFSTEP]
ext a
[GOAL]
case property.refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (forget TopCat).obj S.pt
⊢ ↑((ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }) ≫
          PullbackCone.snd
            (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)))
      a =
    ↑(PullbackCone.snd S) a
[PROOFSTEP]
rw [comp_apply, ContinuousMap.coe_mk]
[GOAL]
case property.refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (forget TopCat).obj S.pt
⊢ ↑(PullbackCone.snd
          (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) (_ : pullbackFst f g ≫ f = pullbackSnd f g ≫ g)))
      { val := (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a),
        property :=
          (_ :
            ↑f (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a).fst =
              ↑g (↑(PullbackCone.fst S) a, ↑(PullbackCone.snd S) a).snd) } =
    ↑(PullbackCone.snd S) a
[PROOFSTEP]
rfl
[GOAL]
case property.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S →
      m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S →
        m =
          ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }
[PROOFSTEP]
intro m h₁ h₂
[GOAL]
case property.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
⊢ m =
    ContinuousMap.mk fun x =>
      { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
        property :=
          (_ :
            ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
              ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) }
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case property.refine'_3.h
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
⊢ ∀ (a : ↑S.pt),
    ↑m a =
      ↑(ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) })
        a
[PROOFSTEP]
intro x
[GOAL]
case property.refine'_3.h
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
x : ↑S.pt
⊢ ↑m x =
    ↑(ContinuousMap.mk fun x =>
          { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
            property :=
              (_ :
                ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                  ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) })
      x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case property.refine'_3.h.a
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
x : ↑S.pt
⊢ ↑(↑m x) =
    ↑(↑(ContinuousMap.mk fun x =>
            { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
              property :=
                (_ :
                  ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                    ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) })
        x)
[PROOFSTEP]
apply Prod.ext
[GOAL]
case property.refine'_3.h.a.h₁
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
x : ↑S.pt
⊢ (↑(↑m x)).fst =
    (↑(↑(ContinuousMap.mk fun x =>
              { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
                property :=
                  (_ :
                    ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                      ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) })
          x)).fst
[PROOFSTEP]
simpa using ConcreteCategory.congr_hom h₁ x
[GOAL]
case property.refine'_3.h.a.h₂
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ PullbackCone.fst (pullbackCone f g) = PullbackCone.fst S
h₂ : m ≫ PullbackCone.snd (pullbackCone f g) = PullbackCone.snd S
x : ↑S.pt
⊢ (↑(↑m x)).snd =
    (↑(↑(ContinuousMap.mk fun x =>
              { val := (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x),
                property :=
                  (_ :
                    ↑f (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).fst =
                      ↑g (↑(PullbackCone.fst S) x, ↑(PullbackCone.snd S) x).snd) })
          x)).snd
[PROOFSTEP]
simpa using ConcreteCategory.congr_hom h₂ x
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.fst = pullbackFst f g
[PROOFSTEP]
simp [pullbackCone, pullbackIsoProdSubtype]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.snd = pullbackSnd f g
[PROOFSTEP]
simp [pullbackCone, pullbackIsoProdSubtype]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst
[PROOFSTEP]
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd
[PROOFSTEP]
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_snd]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ ↑f (↑pullback.fst x, ↑pullback.snd x).fst = ↑g (↑pullback.fst x, ↑pullback.snd x).snd
[PROOFSTEP]
simpa using ConcreteCategory.congr_hom pullback.condition x
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ConcreteCategory.forget.obj (pullback f g)
⊢ ↑(pullbackIsoProdSubtype f g).hom x =
    { val := (↑pullback.fst x, ↑pullback.snd x),
      property := (_ : ↑f (↑pullback.fst x, ↑pullback.snd x).fst = ↑g (↑pullback.fst x, ↑pullback.snd x).snd) }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
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)
⊢ ↑(↑(pullbackIsoProdSubtype f g).hom x) =
    ↑{ val := (↑pullback.fst x, ↑pullback.snd x),
        property := (_ : ↑f (↑pullback.fst x, ↑pullback.snd x).fst = ↑g (↑pullback.fst x, ↑pullback.snd x).snd) }
[PROOFSTEP]
apply Prod.ext
[GOAL]
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)
⊢ (↑(↑(pullbackIsoProdSubtype f g).hom x)).fst =
    (↑{ val := (↑pullback.fst x, ↑pullback.snd x),
          property := (_ : ↑f (↑pullback.fst x, ↑pullback.snd x).fst = ↑g (↑pullback.fst x, ↑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)
⊢ (↑(↑(pullbackIsoProdSubtype f g).hom x)).snd =
    (↑{ val := (↑pullback.fst x, ↑pullback.snd x),
          property := (_ : ↑f (↑pullback.fst x, ↑pullback.snd x).fst = ↑g (↑pullback.fst x, ↑pullback.snd x).snd) }).snd
[PROOFSTEP]
exacts [ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_fst f g) x,
  ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_snd f g) x]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str = induced (↑pullback.fst) X.str ⊓ induced (↑pullback.snd) Y.str
[PROOFSTEP]
let homeo := homeoOfIso (pullbackIsoProdSubtype f g)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // ↑f p.fst = ↑g p.snd }) := homeoOfIso (pullbackIsoProdSubtype f g)
⊢ (pullback f g).str = induced (↑pullback.fst) X.str ⊓ induced (↑pullback.snd) Y.str
[PROOFSTEP]
refine' homeo.inducing.induced.trans _
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // ↑f p.fst = ↑g p.snd }) := homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (topologicalSpace_coe (of { p // ↑f p.fst = ↑g p.snd })) =
    induced (↑pullback.fst) X.str ⊓ induced (↑pullback.snd) Y.str
[PROOFSTEP]
change induced homeo (induced _ ((induced Prod.fst X.str) ⊓ (induced Prod.snd Y.str))) = _
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // ↑f p.fst = ↑g p.snd }) := homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (↑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) =
    induced (↑pullback.fst) X.str ⊓ induced (↑pullback.snd) Y.str
[PROOFSTEP]
simp only [induced_compose, induced_inf]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // ↑f p.fst = ↑g p.snd }) := homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) X.str ⊓
      induced ((Prod.snd ∘ Subtype.val) ∘ ↑(homeoOfIso (pullbackIsoProdSubtype f g))) Y.str =
    induced (↑pullback.fst) X.str ⊓ induced (↑pullback.snd) Y.str
[PROOFSTEP]
congr
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Set.range ↑(prod.lift pullback.fst pullback.snd) = {x | ↑(prod.fst ≫ f) x = ↑(prod.snd ≫ g) x}
[PROOFSTEP]
ext x
[GOAL]
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 ↑(prod.lift pullback.fst pullback.snd) ↔ x ∈ {x | ↑(prod.fst ≫ f) x = ↑(prod.snd ≫ g) x}
[PROOFSTEP]
constructor
[GOAL]
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 ↑(prod.lift pullback.fst pullback.snd) → x ∈ {x | ↑(prod.fst ≫ f) x = ↑(prod.snd ≫ g) x}
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
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)
⊢ ↑(prod.lift pullback.fst pullback.snd) y ∈ {x | ↑(prod.fst ≫ f) x = ↑(prod.snd ≫ g) x}
[PROOFSTEP]
simp only [← comp_apply, Set.mem_setOf_eq]
[GOAL]
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)
⊢ ↑(prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f) y = ↑(prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g) y
[PROOFSTEP]
congr 1
[GOAL]
case h.mp.intro.e_a
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)
⊢ prod.lift pullback.fst pullback.snd ≫ prod.fst ≫ f = prod.lift pullback.fst pullback.snd ≫ prod.snd ≫ g
[PROOFSTEP]
simp [pullback.condition]
[GOAL]
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 | ↑(prod.fst ≫ f) x = ↑(prod.snd ≫ g) x} → x ∈ Set.range ↑(prod.lift pullback.fst pullback.snd)
[PROOFSTEP]
rintro (h : f (_, _).1 = g (_, _).2)
[GOAL]
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 : ↑f (↑prod.fst x, ?m.48880).fst = ↑g (?m.48915, ↑prod.snd x).snd
⊢ x ∈ Set.range ↑(prod.lift pullback.fst pullback.snd)
[PROOFSTEP]
use(pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
[GOAL]
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)
h : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ↑(prod.lift pullback.fst pullback.snd)
      (↑(pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h }) =
    x
[PROOFSTEP]
apply Concrete.limit_ext
[GOAL]
case h.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 : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ∀ (j : Discrete WalkingPair),
    ↑(limit.π (pair X Y) j)
        (↑(prod.lift pullback.fst pullback.snd)
          (↑(pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
      ↑(limit.π (pair X Y) j) x
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case h.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 : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ↑(limit.π (pair X Y) { as := WalkingPair.left })
      (↑(prod.lift pullback.fst pullback.snd)
        (↑(pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ↑(limit.π (pair X Y) { as := WalkingPair.left }) x
[PROOFSTEP]
rw [← comp_apply, prod.comp_lift, ← comp_apply, limit.lift_π]
[GOAL]
case h.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 : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ↑(limit.π (pair X Y) { as := WalkingPair.right })
      (↑(prod.lift pullback.fst pullback.snd)
        (↑(pullbackIsoProdSubtype f g).inv { val := (↑prod.fst x, ↑prod.snd x), property := h })) =
    ↑(limit.π (pair X Y) { as := WalkingPair.right }) x
[PROOFSTEP]
rw [← comp_apply, prod.comp_lift, ← comp_apply, limit.lift_π]
[GOAL]
case h.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 : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ↑(NatTrans.app
          (BinaryFan.mk ((pullbackIsoProdSubtype f g).inv ≫ pullback.fst)
              ((pullbackIsoProdSubtype f g).inv ≫ pullback.snd)).π
          { as := WalkingPair.left })
      { val := (↑prod.fst x, ↑prod.snd x), property := h } =
    ↑(limit.π (pair X Y) { as := WalkingPair.left }) x
[PROOFSTEP]
simp
[GOAL]
case h.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 : ↑f (↑prod.fst x, ↑prod.snd x).fst = ↑g (↑prod.fst x, ↑prod.snd x).snd
⊢ ↑(NatTrans.app
          (BinaryFan.mk ((pullbackIsoProdSubtype f g).inv ≫ pullback.fst)
              ((pullbackIsoProdSubtype f g).inv ≫ pullback.snd)).π
          { as := WalkingPair.right })
      { val := (↑prod.fst x, ↑prod.snd x), property := h } =
    ↑(limit.π (pair X Y) { as := WalkingPair.right }) x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ topologicalSpace_forget (pullback f g) =
    induced (↑(prod.lift pullback.fst pullback.snd)) (topologicalSpace_forget (X ⨯ Y))
[PROOFSTEP]
simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
    ↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂
[PROOFSTEP]
ext
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
⊢ x✝ ∈ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ↔
    x✝ ∈ ↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂
[PROOFSTEP]
constructor
[GOAL]
case h.mp
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
⊢ x✝ ∈ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) →
    x✝ ∈ ↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : (forget TopCat).obj (pullback f₁ f₂)
⊢ ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) y ∈ ↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂
[PROOFSTEP]
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← comp_apply, limit.lift_π, PullbackCone.mk_pt,
  PullbackCone.mk_π_app]
[GOAL]
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : (forget TopCat).obj (pullback f₁ f₂)
⊢ (∃ y_1, ↑i₁ y_1 = ↑(pullback.fst ≫ i₁) y) ∧ ∃ y_1, ↑i₂ y_1 = ↑(pullback.snd ≫ i₂) y
[PROOFSTEP]
simp only [comp_apply, exists_apply_eq_apply, and_self]
[GOAL]
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
⊢ x✝ ∈ ↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂ →
    x✝ ∈ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
[GOAL]
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
⊢ x✝ ∈ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
have : f₁ x₁ = f₂ x₂ := by
  apply (TopCat.mono_iff_injective _).mp H₃
  simp only [← comp_apply, eq₁, eq₂]
  simp only [comp_apply, hx₁, hx₂]
  simp only [← comp_apply, pullback.condition]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
⊢ ↑f₁ x₁ = ↑f₂ x₂
[PROOFSTEP]
apply (TopCat.mono_iff_injective _).mp H₃
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
⊢ ↑i₃ (↑f₁ x₁) = ↑i₃ (↑f₂ x₂)
[PROOFSTEP]
simp only [← comp_apply, eq₁, eq₂]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
⊢ ↑(i₁ ≫ g₁) x₁ = ↑(i₂ ≫ g₂) x₂
[PROOFSTEP]
simp only [comp_apply, hx₁, hx₂]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
⊢ ↑g₁ (↑pullback.fst x✝) = ↑g₂ (↑pullback.snd x✝)
[PROOFSTEP]
simp only [← comp_apply, pullback.condition]
[GOAL]
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ x✝ ∈ Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
use(pullbackIsoProdSubtype f₁ f₂).inv ⟨⟨x₁, x₂⟩, this⟩
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
      (↑(pullbackIsoProdSubtype f₁ f₂).inv { val := (x₁, x₂), property := this }) =
    x✝
[PROOFSTEP]
apply Concrete.limit_ext
[GOAL]
case h.a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ∀ (j : WalkingCospan),
    ↑(limit.π (cospan g₁ g₂) j)
        (↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
          (↑(pullbackIsoProdSubtype f₁ f₂).inv { val := (x₁, x₂), property := this })) =
      ↑(limit.π (cospan g₁ g₂) j) x✝
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case h.a.none
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑(limit.π (cospan g₁ g₂) none)
      (↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
        (↑(pullbackIsoProdSubtype f₁ f₂).inv { val := (x₁, x₂), property := this })) =
    ↑(limit.π (cospan g₁ g₂) none) x✝
[PROOFSTEP]
simp only [← comp_apply, Category.assoc, limit.lift_π, PullbackCone.mk_π_app_one]
[GOAL]
case h.a.some.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑(limit.π (cospan g₁ g₂) (some WalkingPair.left))
      (↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
        (↑(pullbackIsoProdSubtype f₁ f₂).inv { val := (x₁, x₂), property := this })) =
    ↑(limit.π (cospan g₁ g₂) (some WalkingPair.left)) x✝
[PROOFSTEP]
simp only [← comp_apply, Category.assoc, limit.lift_π, PullbackCone.mk_π_app_one]
[GOAL]
case h.a.some.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑(limit.π (cospan g₁ g₂) (some WalkingPair.right))
      (↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
        (↑(pullbackIsoProdSubtype f₁ f₂).inv { val := (x₁, x₂), property := this })) =
    ↑(limit.π (cospan g₁ g₂) (some WalkingPair.right)) x✝
[PROOFSTEP]
simp only [← comp_apply, Category.assoc, limit.lift_π, PullbackCone.mk_π_app_one]
[GOAL]
case h.a.none
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑((pullbackIsoProdSubtype f₁ f₂).inv ≫ pullback.fst ≫ i₁ ≫ g₁) { val := (x₁, x₂), property := this } =
    ↑(limit.π (cospan g₁ g₂) none) x✝
[PROOFSTEP]
simp only [cospan_one, pullbackIsoProdSubtype_inv_fst_assoc, comp_apply, pullbackFst_apply, hx₁]
[GOAL]
case h.a.none
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑g₁ (↑pullback.fst x✝) = ↑(limit.π (cospan g₁ g₂) none) x✝
[PROOFSTEP]
rw [← limit.w _ WalkingCospan.Hom.inl, cospan_map_inl, comp_apply (g := g₁)]
[GOAL]
case h.a.some.left
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑((pullbackIsoProdSubtype f₁ f₂).inv ≫
          NatTrans.app
            (PullbackCone.mk (pullback.fst ≫ i₁) (pullback.snd ≫ i₂)
                (_ : (pullback.fst ≫ i₁) ≫ g₁ = (pullback.snd ≫ i₂) ≫ g₂)).π
            (some WalkingPair.left))
      { val := (x₁, x₂), property := this } =
    ↑(limit.π (cospan g₁ g₂) (some WalkingPair.left)) x✝
[PROOFSTEP]
simp [hx₁]
[GOAL]
case h.a.some.right
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ : TopCat
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : (forget TopCat).obj (pullback g₁ g₂)
x₁ : (forget TopCat).obj W
hx₁ : ↑i₁ x₁ = ↑pullback.fst x✝
x₂ : (forget TopCat).obj X
hx₂ : ↑i₂ x₂ = ↑pullback.snd x✝
this : ↑f₁ x₁ = ↑f₂ x₂
⊢ ↑((pullbackIsoProdSubtype f₁ f₂).inv ≫
          NatTrans.app
            (PullbackCone.mk (pullback.fst ≫ i₁) (pullback.snd ≫ i₂)
                (_ : (pullback.fst ≫ i₁) ≫ g₁ = (pullback.snd ≫ i₂) ≫ g₂)).π
            (some WalkingPair.right))
      { val := (x₁, x₂), property := this } =
    ↑(limit.π (cospan g₁ g₂) (some WalkingPair.right)) x✝
[PROOFSTEP]
simp [hx₂]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ↑pullback.fst = {x | ∃ y, ↑f x = ↑g y}
[PROOFSTEP]
ext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj X
⊢ x ∈ Set.range ↑pullback.fst ↔ x ∈ {x | ∃ y, ↑f x = ↑g y}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj X
⊢ x ∈ Set.range ↑pullback.fst → x ∈ {x | ∃ y, ↑f x = ↑g y}
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case h.mp.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 (pullback f g)
⊢ ↑pullback.fst y ∈ {x | ∃ y, ↑f x = ↑g y}
[PROOFSTEP]
use(pullback.snd : pullback f g ⟶ _) y
[GOAL]
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 (pullback f g)
⊢ ↑f (↑pullback.fst y) = ↑g (↑pullback.snd y)
[PROOFSTEP]
exact ConcreteCategory.congr_hom pullback.condition y
[GOAL]
case h.mpr
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj X
⊢ x ∈ {x | ∃ y, ↑f x = ↑g y} → x ∈ Set.range ↑pullback.fst
[PROOFSTEP]
rintro ⟨y, eq⟩
[GOAL]
case h.mpr.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 X
y : ↑Y
eq : ↑f x = ↑g y
⊢ x ∈ Set.range ↑pullback.fst
[PROOFSTEP]
use(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : (forget TopCat).obj X
y : ↑Y
eq : ↑f x = ↑g y
⊢ ↑pullback.fst (↑(pullbackIsoProdSubtype f g).inv { val := (x, y), property := eq }) = x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ↑pullback.snd = {y | ∃ x, ↑f x = ↑g y}
[PROOFSTEP]
ext y
[GOAL]
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 ↑pullback.snd ↔ y ∈ {y | ∃ x, ↑f x = ↑g y}
[PROOFSTEP]
constructor
[GOAL]
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 ↑pullback.snd → y ∈ {y | ∃ x, ↑f x = ↑g y}
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
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)
⊢ ↑pullback.snd x ∈ {y | ∃ x, ↑f x = ↑g y}
[PROOFSTEP]
use(pullback.fst : pullback f g ⟶ _) x
[GOAL]
case h
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)
⊢ ↑f (↑pullback.fst x) = ↑g (↑pullback.snd x)
[PROOFSTEP]
exact ConcreteCategory.congr_hom pullback.condition x
[GOAL]
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, ↑f x = ↑g y} → y ∈ Set.range ↑pullback.snd
[PROOFSTEP]
rintro ⟨x, eq⟩
[GOAL]
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 : ↑f x = ↑g y
⊢ y ∈ Set.range ↑pullback.snd
[PROOFSTEP]
use(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
[GOAL]
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
x : ↑X
eq : ↑f x = ↑g y
⊢ ↑pullback.snd (↑(pullbackIsoProdSubtype f g).inv { val := (x, y), property := eq }) = y
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ↑i₁
H₂ : Embedding ↑i₂
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
refine'
  embedding_of_embedding_compose (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift pullback.fst pullback.snd : pullback g₁ g₂ ⟶ Y ⨯ Z) from
      ContinuousMap.continuous_toFun _)
    _
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ↑i₁
H₂ : Embedding ↑i₂
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding (↑(prod.lift pullback.fst pullback.snd) ∘ ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
[PROOFSTEP]
suffices Embedding (prod.lift pullback.fst pullback.snd ≫ Limits.prod.map i₁ i₂ : pullback f₁ f₂ ⟶ _) by
  simpa [← coe_comp] using this
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ↑i₁
H₂ : Embedding ↑i₂
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
this : Embedding ↑(prod.lift pullback.fst pullback.snd ≫ prod.map i₁ i₂)
⊢ Embedding (↑(prod.lift pullback.fst pullback.snd) ∘ ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
[PROOFSTEP]
simpa [← coe_comp] using this
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ↑i₁
H₂ : Embedding ↑i₂
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ↑(prod.lift pullback.fst pullback.snd ≫ prod.map i₁ i₂)
[PROOFSTEP]
rw [coe_comp]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : Embedding ↑i₁
H₂ : Embedding ↑i₂
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding (↑(prod.map i₁ i₂) ∘ ↑(prod.lift pullback.fst pullback.snd))
[PROOFSTEP]
refine Embedding.comp (embedding_prod_map H₁ H₂) (embedding_pullback_to_prod _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ OpenEmbedding ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
constructor
[GOAL]
case toEmbedding
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Embedding ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
[PROOFSTEP]
apply pullback_map_embedding_of_embeddings f₁ f₂ g₁ g₂ H₁.toEmbedding H₂.toEmbedding i₃ eq₁ eq₂
[GOAL]
case open_range
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ↑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
[PROOFSTEP]
rw [range_pullback_map]
[GOAL]
case open_range
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (↑pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑pullback.snd ⁻¹' Set.range ↑i₂)
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case open_range.h₁
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (↑pullback.fst ⁻¹' Set.range ↑i₁)
[PROOFSTEP]
apply Continuous.isOpen_preimage
[GOAL]
case open_range.h₂
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (↑pullback.snd ⁻¹' Set.range ↑i₂)
[PROOFSTEP]
apply Continuous.isOpen_preimage
[GOAL]
case open_range.h₁.self
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ↑pullback.fst
[PROOFSTEP]
apply ContinuousMap.continuous_toFun
[GOAL]
case open_range.h₁.a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ↑i₁)
[PROOFSTEP]
exact H₁.open_range
[GOAL]
case open_range.h₂.self
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ↑pullback.snd
[PROOFSTEP]
apply ContinuousMap.continuous_toFun
[GOAL]
case open_range.h₂.a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z✝ W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : OpenEmbedding ↑i₁
H₂ : OpenEmbedding ↑i₂
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ↑i₂)
[PROOFSTEP]
exact H₂.open_range
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : Embedding ↑f
g : Y ⟶ S
⊢ Embedding ↑pullback.snd
[PROOFSTEP]
convert
  (homeoOfIso (asIso (pullback.snd : pullback (𝟙 S) g ⟶ _))).embedding.comp
    (pullback_map_embedding_of_embeddings (i₂ := 𝟙 Y) f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).embedding (𝟙 _) rfl
      (by simp))
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : Embedding ↑f
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : Embedding ↑f
g : Y ⟶ S
e_2✝ : (forget TopCat).obj Y = ↑Y
⊢ ↑pullback.snd =
    ↑(homeoOfIso (asIso pullback.snd)) ∘
      ↑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = 𝟙 Y ≫ g))
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : Embedding ↑f
g : Y ⟶ S
e_2✝ : (forget TopCat).obj Y = ↑Y
⊢ ↑pullback.snd =
    ↑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = 𝟙 Y ≫ g) ≫ (asIso pullback.snd).hom)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ↑g
⊢ Embedding ↑pullback.fst
[PROOFSTEP]
convert
  (homeoOfIso (asIso (pullback.fst : pullback f (𝟙 S) ⟶ _))).embedding.comp
    (pullback_map_embedding_of_embeddings (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).embedding H (𝟙 _) rfl
      (by simp))
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ↑g
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ↑g
e_2✝ : (forget TopCat).obj X = ↑X
⊢ ↑pullback.fst =
    ↑(homeoOfIso (asIso pullback.fst)) ∘
      ↑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S))
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ↑g
e_2✝ : (forget TopCat).obj X = ↑X
⊢ ↑pullback.fst =
    ↑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S) ≫ (asIso pullback.fst).hom)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : Embedding ↑f
H₂ : Embedding ↑g
⊢ Embedding ↑(limit.π (cospan f g) WalkingCospan.one)
[PROOFSTEP]
convert H₂.comp (snd_embedding_of_left_embedding H₁ g)
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : Embedding ↑f
H₂ : Embedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑g ∘ ↑pullback.snd
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : Embedding ↑f
H₂ : Embedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
congr
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : Embedding ↑f
H₂ : Embedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
rw [← limit.w _ WalkingCospan.Hom.inr]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : Embedding ↑f
H₂ : Embedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : OpenEmbedding ↑f
g : Y ⟶ S
⊢ OpenEmbedding ↑pullback.snd
[PROOFSTEP]
convert
  (homeoOfIso (asIso (pullback.snd : pullback (𝟙 S) g ⟶ _))).openEmbedding.comp
    (pullback_map_openEmbedding_of_open_embeddings (i₂ := 𝟙 Y) f g (𝟙 _) g H (homeoOfIso (Iso.refl _)).openEmbedding
      (𝟙 _) rfl (by simp))
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : OpenEmbedding ↑f
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : OpenEmbedding ↑f
g : Y ⟶ S
e_2✝ : (forget TopCat).obj Y = ↑Y
⊢ ↑pullback.snd =
    ↑(homeoOfIso (asIso pullback.snd)) ∘
      ↑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = 𝟙 Y ≫ g))
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
H : OpenEmbedding ↑f
g : Y ⟶ S
e_2✝ : (forget TopCat).obj Y = ↑Y
⊢ ↑pullback.snd =
    ↑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = 𝟙 Y ≫ g) ≫ (asIso pullback.snd).hom)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : OpenEmbedding ↑g
⊢ OpenEmbedding ↑pullback.fst
[PROOFSTEP]
convert
  (homeoOfIso (asIso (pullback.fst : pullback f (𝟙 S) ⟶ _))).openEmbedding.comp
    (pullback_map_openEmbedding_of_open_embeddings (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).openEmbedding H
      (𝟙 _) rfl (by simp))
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : OpenEmbedding ↑g
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj X = ↑X
⊢ ↑pullback.fst =
    ↑(homeoOfIso (asIso pullback.fst)) ∘
      ↑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S))
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj X = ↑X
⊢ ↑pullback.fst =
    ↑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S) ≫ (asIso pullback.fst).hom)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ↑f
H₂ : OpenEmbedding ↑g
⊢ OpenEmbedding ↑(limit.π (cospan f g) WalkingCospan.one)
[PROOFSTEP]
convert H₂.comp (snd_openEmbedding_of_left_openEmbedding H₁ g)
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ↑f
H₂ : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑g ∘ ↑pullback.snd
[PROOFSTEP]
erw [← coe_comp]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ↑f
H₂ : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
congr
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ↑f
H₂ : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.one) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
rw [← (limit.w _ WalkingCospan.Hom.inr)]
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ↑f
H₂ : OpenEmbedding ↑g
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ ↑(limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr) = ↑(pullback.snd ≫ g)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ↑g
H : Set.range ↑f ⊆ Set.range ↑g
⊢ IsIso pullback.fst
[PROOFSTEP]
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 }
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ↑g
H : Set.range ↑f ⊆ Set.range ↑g
x : ↑X
⊢ x ∈ Set.range ↑pullback.fst
[PROOFSTEP]
rw [pullback_fst_range]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ↑g
H : Set.range ↑f ⊆ Set.range ↑g
x : ↑X
⊢ x ∈ {x | ∃ y, ↑f x = ↑g y}
[PROOFSTEP]
exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : Embedding ↑g
H : Set.range ↑f ⊆ Set.range ↑g
esto : ↑(pullback f g) ≃ₜ ↑X :=
  Homeomorph.trans (Homeomorph.ofEmbedding ↑pullback.fst (_ : Embedding ↑pullback.fst))
    (Homeomorph.mk
      { toFun := Subtype.val, invFun := fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.fst) },
        left_inv :=
          (_ :
            ∀ (x : ↑(Set.range ↑pullback.fst)),
              (fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.fst) }) ↑x = x),
        right_inv :=
          (_ :
            ∀ (x : ↑X),
              ↑((fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.fst) }) x) =
                ↑((fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.fst) }) x)) })
⊢ IsIso pullback.fst
[PROOFSTEP]
convert IsIso.of_iso (isoOfHomeo esto)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
hf : Embedding ↑f
g : Y ⟶ S
H : Set.range ↑g ⊆ Set.range ↑f
⊢ IsIso pullback.snd
[PROOFSTEP]
let esto : (pullback f g : TopCat) ≃ₜ Y :=
  (Homeomorph.ofEmbedding _ (snd_embedding_of_left_embedding hf g)).trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by
          rw [pullback_snd_range]
          exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩⟩
      left_inv := fun ⟨_, _⟩ => rfl
      right_inv := fun x => rfl }
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
hf : Embedding ↑f
g : Y ⟶ S
H : Set.range ↑g ⊆ Set.range ↑f
x : ↑Y
⊢ x ∈ Set.range ↑pullback.snd
[PROOFSTEP]
rw [pullback_snd_range]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
hf : Embedding ↑f
g : Y ⟶ S
H : Set.range ↑g ⊆ Set.range ↑f
x : ↑Y
⊢ x ∈ {y | ∃ x, ↑f x = ↑g y}
[PROOFSTEP]
exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩
[GOAL]
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
hf : Embedding ↑f
g : Y ⟶ S
H : Set.range ↑g ⊆ Set.range ↑f
esto : ↑(pullback f g) ≃ₜ ↑Y :=
  Homeomorph.trans (Homeomorph.ofEmbedding ↑pullback.snd (_ : Embedding ↑pullback.snd))
    (Homeomorph.mk
      { toFun := Subtype.val, invFun := fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.snd) },
        left_inv :=
          (_ :
            ∀ (x : ↑(Set.range ↑pullback.snd)),
              (fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.snd) }) ↑x = x),
        right_inv :=
          (_ :
            ∀ (x : ↑Y),
              ↑((fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.snd) }) x) =
                ↑((fun x => { val := x, property := (_ : x ∈ Set.range ↑pullback.snd) }) x)) })
⊢ IsIso pullback.snd
[PROOFSTEP]
convert IsIso.of_iso (isoOfHomeo esto)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
⊢ ↑pullback.snd '' (↑pullback.fst ⁻¹' U) = ↑g ⁻¹' (↑f '' U)
[PROOFSTEP]
ext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
⊢ x ∈ ↑pullback.snd '' (↑pullback.fst ⁻¹' U) ↔ x ∈ ↑g ⁻¹' (↑f '' U)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
⊢ x ∈ ↑pullback.snd '' (↑pullback.fst ⁻¹' U) → x ∈ ↑g ⁻¹' (↑f '' U)
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case h.mp.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
y : (forget TopCat).obj (pullback f g)
hy : y ∈ ↑pullback.fst ⁻¹' U
⊢ ↑pullback.snd y ∈ ↑g ⁻¹' (↑f '' U)
[PROOFSTEP]
exact ⟨(pullback.fst : pullback f g ⟶ _) y, hy, ConcreteCategory.congr_hom pullback.condition y⟩
[GOAL]
case h.mpr
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
⊢ x ∈ ↑g ⁻¹' (↑f '' U) → x ∈ ↑pullback.snd '' (↑pullback.fst ⁻¹' U)
[PROOFSTEP]
rintro ⟨y, hy, eq⟩
[GOAL]
case h.mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
y : (forget TopCat).obj X
hy : y ∈ U
eq : ↑f y = ↑g x
⊢ x ∈ ↑pullback.snd '' (↑pullback.fst ⁻¹' U)
[PROOFSTEP]
exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
y : (forget TopCat).obj X
hy : y ∈ U
eq : ↑f y = ↑g x
⊢ ↑(pullbackIsoProdSubtype f g).inv { val := (y, x), property := eq } ∈ ↑pullback.fst ⁻¹' U
[PROOFSTEP]
simpa
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : (forget TopCat).obj Y
y : (forget TopCat).obj X
hy : y ∈ U
eq : ↑f y = ↑g x
⊢ ↑pullback.snd (↑(pullbackIsoProdSubtype f g).inv { val := (y, x), property := eq }) = x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
⊢ ↑pullback.fst '' (↑pullback.snd ⁻¹' U) = ↑f ⁻¹' (↑g '' U)
[PROOFSTEP]
ext x
[GOAL]
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 ∈ ↑pullback.fst '' (↑pullback.snd ⁻¹' U) ↔ x ∈ ↑f ⁻¹' (↑g '' U)
[PROOFSTEP]
constructor
[GOAL]
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 ∈ ↑pullback.fst '' (↑pullback.snd ⁻¹' U) → x ∈ ↑f ⁻¹' (↑g '' U)
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
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 ∈ ↑pullback.snd ⁻¹' U
⊢ ↑pullback.fst y ∈ ↑f ⁻¹' (↑g '' U)
[PROOFSTEP]
exact ⟨(pullback.snd : pullback f g ⟶ _) y, hy, (ConcreteCategory.congr_hom pullback.condition y).symm⟩
[GOAL]
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 ∈ ↑f ⁻¹' (↑g '' U) → x ∈ ↑pullback.fst '' (↑pullback.snd ⁻¹' U)
[PROOFSTEP]
rintro ⟨y, hy, eq⟩
[GOAL]
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 : ↑g y = ↑f x
⊢ x ∈ ↑pullback.fst '' (↑pullback.snd ⁻¹' U)
[PROOFSTEP]
exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, by simpa, by simp⟩
[GOAL]
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 : ↑g y = ↑f x
⊢ ↑(pullbackIsoProdSubtype f g).inv { val := (x, y), property := (_ : ↑f x = ↑g y) } ∈ ↑pullback.snd ⁻¹' U
[PROOFSTEP]
simpa
[GOAL]
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 : ↑g y = ↑f x
⊢ ↑pullback.fst (↑(pullbackIsoProdSubtype f g).inv { val := (x, y), property := (_ : ↑f x = ↑g y) }) = x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
⊢ c.pt.str = ⨆ (j : J), coinduced (↑(NatTrans.app c.ι j)) (F.obj j).str
[PROOFSTEP]
let homeo := homeoOfIso (hc.coconePointUniqueUpToIso (colimitCoconeIsColimit F))
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
⊢ c.pt.str = ⨆ (j : J), coinduced (↑(NatTrans.app c.ι j)) (F.obj j).str
[PROOFSTEP]
ext
[GOAL]
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen x✝ ↔ IsOpen x✝
[PROOFSTEP]
refine' homeo.symm.isOpen_preimage.symm.trans (Iff.trans _ isOpen_iSup_iff.symm)
[GOAL]
case a.h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
c : Cocone F
hc : IsColimit c
homeo : ↑c.pt ≃ₜ ↑(colimitCocone F).pt := homeoOfIso (IsColimit.coconePointUniqueUpToIso hc (colimitCoconeIsColimit F))
x✝ : Set ↑c.pt
⊢ IsOpen (↑(Homeomorph.symm homeo) ⁻¹' x✝) ↔ ∀ (i : J), IsOpen x✝
[PROOFSTEP]
exact isOpen_iSup_iff
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
⊢ IsOpen U ↔ ∀ (j : J), IsOpen (↑(colimit.ι F j) ⁻¹' U)
[PROOFSTEP]
dsimp [topologicalSpace_coe]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
⊢ IsOpen U ↔ ∀ (j : J), IsOpen (↑(colimit.ι F j) ⁻¹' U)
[PROOFSTEP]
conv_lhs => rw [colimit_topology F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
| IsOpen U
[PROOFSTEP]
rw [colimit_topology F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
| IsOpen U
[PROOFSTEP]
rw [colimit_topology F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
| IsOpen U
[PROOFSTEP]
rw [colimit_topology F]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
U : Set ↑(colimit F)
⊢ IsOpen U ↔ ∀ (j : J), IsOpen (↑(colimit.ι F j) ⁻¹' U)
[PROOFSTEP]
exact isOpen_iSup_iff
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ IsOpen U ↔ IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
rw [colimit_isOpen_iff]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen (↑(colimit.ι F j) ⁻¹' U)) ↔ IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
constructor
[GOAL]
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ (∀ (j : WalkingParallelPair), IsOpen (↑(colimit.ι F j) ⁻¹' U)) → IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
intro H
[GOAL]
case mp
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : ∀ (j : WalkingParallelPair), IsOpen (↑(colimit.ι F j) ⁻¹' U)
⊢ IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
exact H _
[GOAL]
case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
⊢ IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U) → ∀ (j : WalkingParallelPair), IsOpen (↑(colimit.ι F j) ⁻¹' U)
[PROOFSTEP]
intro H j
[GOAL]
case mpr
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
j : WalkingParallelPair
⊢ IsOpen (↑(colimit.ι F j) ⁻¹' U)
[PROOFSTEP]
cases j
[GOAL]
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen (↑(colimit.ι F WalkingParallelPair.zero) ⁻¹' U)
[PROOFSTEP]
rw [← colimit.w F WalkingParallelPairHom.left]
[GOAL]
case mpr.zero
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen (↑(F.map WalkingParallelPairHom.left ≫ colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
exact (F.map WalkingParallelPairHom.left).continuous_toFun.isOpen_preimage _ H
[GOAL]
case mpr.one
J : Type v
inst✝ : SmallCategory J
F : WalkingParallelPair ⥤ TopCat
U : Set ↑(colimit F)
H : IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
⊢ IsOpen (↑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
[PROOFSTEP]
exact H
