[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
⊢ ∀ (s : Cone (Discrete.functor α)) (m : s.pt ⟶ (piFan α).pt),
    (∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app s.π j) →
      m = (fun S => ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) s
[PROOFSTEP]
intro S m h
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
⊢ m = (fun S => ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) S
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
⊢ ∀ (a : ↑S.pt), ↑m a = ↑((fun S => ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) S) a
[PROOFSTEP]
intro x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
x : ↑S.pt
⊢ ↑m x = ↑((fun S => ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) S) x
[PROOFSTEP]
funext i
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
x : ↑S.pt
i : ι
⊢ ↑m x i = ↑((fun S => ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) S) x i
[PROOFSTEP]
dsimp
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
x : ↑S.pt
i : ι
⊢ ↑m x i = ↑(ContinuousMap.mk fun s i => ↑(NatTrans.app S.π { as := i }) s) x i
[PROOFSTEP]
rw [ContinuousMap.coe_mk, ← h ⟨i⟩]
[GOAL]
case h.h
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan α).pt
h : ∀ (j : Discrete ι), m ≫ NatTrans.app (piFan α).π j = NatTrans.app S.π j
x : ↑S.pt
i : ι
⊢ ↑m x i = ↑(m ≫ NatTrans.app (piFan α).π { as := i }) x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ (piIsoPi α).inv ≫ Pi.π α i = piπ α i
[PROOFSTEP]
simp [piIsoPi]
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
⊢ ↑(piIsoPi α).hom x i = ↑(Pi.π α i) x
[PROOFSTEP]
have := piIsoPi_inv_π α i
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : (piIsoPi α).inv ≫ Pi.π α i = piπ α i
⊢ ↑(piIsoPi α).hom x i = ↑(Pi.π α i) x
[PROOFSTEP]
rw [Iso.inv_comp_eq] at this 
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(∏ α)
this : Pi.π α i = (piIsoPi α).hom ≫ piπ α i
⊢ ↑(piIsoPi α).hom x i = ↑(Pi.π α i) x
[PROOFSTEP]
exact ConcreteCategory.congr_hom this x
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ α i ⟶ of ((i : ι) × ↑(α i))
[PROOFSTEP]
refine ContinuousMap.mk ?_ ?_
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ ↑(α i) → ↑(of ((i : ι) × ↑(α i)))
[PROOFSTEP]
dsimp
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ ↑(α i) → (i : ι) × ↑(α i)
[PROOFSTEP]
apply Sigma.mk i
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ Continuous (id (Sigma.mk i))
[PROOFSTEP]
dsimp
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ Continuous (Sigma.mk i)
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
s : Cocone (Discrete.functor β)
j : Discrete ι
⊢ NatTrans.app (sigmaCofan β).ι j ≫ (fun S => ContinuousMap.mk fun s => ↑(NatTrans.app S.ι { as := s.fst }) s.snd) s =
    NatTrans.app s.ι j
[PROOFSTEP]
cases j
[GOAL]
case mk
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
s : Cocone (Discrete.functor β)
as✝ : ι
⊢ NatTrans.app (sigmaCofan β).ι { as := as✝ } ≫
      (fun S => ContinuousMap.mk fun s => ↑(NatTrans.app S.ι { as := s.fst }) s.snd) s =
    NatTrans.app s.ι { as := as✝ }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
⊢ ∀ (s : Cocone (Discrete.functor β)) (m : (sigmaCofan β).pt ⟶ s.pt),
    (∀ (j : Discrete ι), NatTrans.app (sigmaCofan β).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun S => ContinuousMap.mk fun s => ↑(NatTrans.app S.ι { as := s.fst }) s.snd) s
[PROOFSTEP]
intro S m h
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), NatTrans.app (sigmaCofan β).ι j ≫ m = NatTrans.app S.ι j
⊢ m = (fun S => ContinuousMap.mk fun s => ↑(NatTrans.app S.ι { as := s.fst }) s.snd) S
[PROOFSTEP]
ext ⟨i, x⟩
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), NatTrans.app (sigmaCofan β).ι j ≫ m = NatTrans.app S.ι j
i : ι
x : ↑(β i)
⊢ ↑m { fst := i, snd := x } =
    ↑((fun S => ContinuousMap.mk fun s => ↑(NatTrans.app S.ι { as := s.fst }) s.snd) S) { fst := i, snd := x }
[PROOFSTEP]
simp only [comp_app, hom_apply, ← h ⟨i⟩]
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
ι : Type v
β : ι → TopCatMax
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), NatTrans.app (sigmaCofan β).ι j ≫ m = NatTrans.app S.ι j
i : ι
x : ↑(β i)
⊢ ContinuousMap.toFun m { fst := i, snd := x } = ContinuousMap.toFun (NatTrans.app (sigmaCofan β).ι { as := i } ≫ m) x
[PROOFSTEP]
congr
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
⊢ Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i
[PROOFSTEP]
simp [sigmaIsoSigma]
[GOAL]
J : Type v
inst✝ : SmallCategory J
ι : Type v
α : ι → TopCatMax
i : ι
x : ↑(α i)
⊢ ↑(sigmaIsoSigma α).inv { fst := i, snd := x } = ↑(Sigma.ι α i) x
[PROOFSTEP]
rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
⊢ C.pt.str = ⨅ (j : J), induced (↑(NatTrans.app C.π j)) (F.obj j).str
[PROOFSTEP]
let homeo := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ C.pt.str = ⨅ (j : J), induced (↑(NatTrans.app C.π j)) (F.obj j).str
[PROOFSTEP]
refine' homeo.inducing.induced.trans _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (topologicalSpace_coe (limitConeInfi F).pt) =
    ⨅ (j : J), induced (↑(NatTrans.app C.π j)) (F.obj j).str
[PROOFSTEP]
change induced homeo (⨅ j : J, _) = _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (⨅ (j : J), induced (NatTrans.app (Types.limitCone (F ⋙ forget TopCat)).π j) (F.obj j).str) =
    ⨅ (j : J), induced (↑(NatTrans.app C.π j)) (F.obj j).str
[PROOFSTEP]
simp [induced_iInf, induced_compose]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ ⨅ (i : J),
      induced
        (NatTrans.app (Types.limitCone (F ⋙ forget TopCat)).π i ∘
          ↑(homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))))
        (F.obj i).str =
    ⨅ (j : J), induced (↑(NatTrans.app C.π j)) (F.obj j).str
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ Continuous Prod.fst
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ Continuous Prod.snd
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (j : Discrete WalkingPair),
    (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) s ≫
        NatTrans.app (prodBinaryFan X Y).π j =
      NatTrans.app s.π j
[PROOFSTEP]
rintro S (_ | _)
[GOAL]
case mk.left
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S ≫
      NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.left } =
    NatTrans.app S.π { as := WalkingPair.left }
[PROOFSTEP]
{dsimp; ext; rfl
}
[GOAL]
case mk.left
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S ≫
      NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.left } =
    NatTrans.app S.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp
[GOAL]
case mk.left
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) ≫ BinaryFan.fst (prodBinaryFan X Y) =
    BinaryFan.fst S
[PROOFSTEP]
ext
[GOAL]
case mk.left.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
x✝ : (forget TopCat).obj S.pt
⊢ ↑((ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) ≫ BinaryFan.fst (prodBinaryFan X Y)) x✝ =
    ↑(BinaryFan.fst S) x✝
[PROOFSTEP]
rfl
[GOAL]
case mk.right
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S ≫
      NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.right } =
    NatTrans.app S.π { as := WalkingPair.right }
[PROOFSTEP]
{dsimp; ext; rfl
}
[GOAL]
case mk.right
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S ≫
      NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.right } =
    NatTrans.app S.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp
[GOAL]
case mk.right
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
⊢ (ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) ≫ BinaryFan.snd (prodBinaryFan X Y) =
    BinaryFan.snd S
[PROOFSTEP]
ext
[GOAL]
case mk.right.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
x✝ : (forget TopCat).obj S.pt
⊢ ↑((ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) ≫ BinaryFan.snd (prodBinaryFan X Y)) x✝ =
    ↑(BinaryFan.snd S) x✝
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (m : s.pt ⟶ (prodBinaryFan X Y).pt),
    (∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (prodBinaryFan X Y).π j = NatTrans.app s.π j) →
      m = (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) s
[PROOFSTEP]
intro S m h
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (prodBinaryFan X Y).π j = NatTrans.app S.π j
⊢ m = (fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S
[PROOFSTEP]
refine' ContinuousMap.ext (fun (x : ↥(S.pt)) => Prod.ext _ _)
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (prodBinaryFan X Y).π j = NatTrans.app S.π j
x : ↑S.pt
⊢ (↑m x).fst = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).fst
[PROOFSTEP]
specialize h ⟨WalkingPair.left⟩
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
x : ↑S.pt
h : m ≫ NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.left } = NatTrans.app S.π { as := WalkingPair.left }
⊢ (↑m x).fst = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).fst
[PROOFSTEP]
apply_fun fun e => e x at h 
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
x : ↑S.pt
h :
  ↑(m ≫ NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.left }) x =
    ↑(NatTrans.app S.π { as := WalkingPair.left }) x
⊢ (↑m x).fst = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).fst
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app (prodBinaryFan X Y).π j = NatTrans.app S.π j
x : ↑S.pt
⊢ (↑m x).snd = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).snd
[PROOFSTEP]
specialize h ⟨WalkingPair.right⟩
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
x : ↑S.pt
h : m ≫ NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.right } = NatTrans.app S.π { as := WalkingPair.right }
⊢ (↑m x).snd = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).snd
[PROOFSTEP]
apply_fun fun e => e x at h 
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (prodBinaryFan X Y).pt
x : ↑S.pt
h :
  ↑(m ≫ NatTrans.app (prodBinaryFan X Y).π { as := WalkingPair.right }) x =
    ↑(NatTrans.app S.π { as := WalkingPair.right }) x
⊢ (↑m x).snd = (↑((fun S => ContinuousMap.mk fun s => (↑(BinaryFan.fst S) s, ↑(BinaryFan.snd S) s)) S) x).snd
[PROOFSTEP]
exact h
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (prodIsoProd X Y).hom ≫ prodFst = prod.fst
[PROOFSTEP]
simp [← Iso.eq_inv_comp, prodIsoProd]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ prodFst = BinaryFan.fst (prodBinaryFan X Y)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (prodIsoProd X Y).hom ≫ prodSnd = prod.snd
[PROOFSTEP]
simp [← Iso.eq_inv_comp, prodIsoProd]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ prodSnd = BinaryFan.snd (prodBinaryFan X Y)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ↑(prodIsoProd X Y).hom x = (↑prod.fst x, ↑prod.snd x)
[PROOFSTEP]
apply Prod.ext
[GOAL]
case h₁
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ (↑(prodIsoProd X Y).hom x).fst = (↑prod.fst x, ↑prod.snd x).fst
[PROOFSTEP]
exact ConcreteCategory.congr_hom (prodIsoProd_hom_fst X Y) x
[GOAL]
case h₂
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ (↑(prodIsoProd X Y).hom x).snd = (↑prod.fst x, ↑prod.snd x).snd
[PROOFSTEP]
exact ConcreteCategory.congr_hom (prodIsoProd_hom_snd X Y) x
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (prodIsoProd X Y).inv ≫ prod.fst = prodFst
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (prodIsoProd X Y).inv ≫ prod.snd = prodSnd
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ (X ⨯ Y).str = induced (↑prod.fst) X.str ⊓ induced (↑prod.snd) Y.str
[PROOFSTEP]
let homeo := homeoOfIso (prodIsoProd X Y)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ (X ⨯ Y).str = induced (↑prod.fst) X.str ⊓ induced (↑prod.snd) Y.str
[PROOFSTEP]
refine' homeo.inducing.induced.trans _
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (topologicalSpace_coe (of (↑X × ↑Y))) = induced (↑prod.fst) X.str ⊓ induced (↑prod.snd) Y.str
[PROOFSTEP]
change induced homeo (_ ⊓ _) = _
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (↑homeo) (induced Prod.fst (topologicalSpace_coe X) ⊓ induced Prod.snd (topologicalSpace_coe Y)) =
    induced (↑prod.fst) X.str ⊓ induced (↑prod.snd) Y.str
[PROOFSTEP]
simp [induced_compose]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (prodIsoProd X Y)
⊢ induced (Prod.fst ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe X) ⊓
      induced (Prod.snd ∘ ↑(homeoOfIso (prodIsoProd X Y))) (topologicalSpace_coe Y) =
    induced (↑prod.fst) X.str ⊓ induced (↑prod.snd) Y.str
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
⊢ Set.range ↑(prod.map f g) = ↑prod.fst ⁻¹' Set.range ↑f ∩ ↑prod.snd ⁻¹' Set.range ↑g
[PROOFSTEP]
ext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ↑(prod.map f g) ↔ x ∈ ↑prod.fst ⁻¹' Set.range ↑f ∩ ↑prod.snd ⁻¹' Set.range ↑g
[PROOFSTEP]
constructor
[GOAL]
case h.mp
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ Set.range ↑(prod.map f g) → x ∈ ↑prod.fst ⁻¹' Set.range ↑f ∩ ↑prod.snd ⁻¹' Set.range ↑g
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ ↑(prod.map f g) y ∈ ↑prod.fst ⁻¹' Set.range ↑f ∩ ↑prod.snd ⁻¹' Set.range ↑g
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_range, Set.mem_inter_iff, ← comp_apply]
[GOAL]
case h.mp.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : (forget TopCat).obj (W ⨯ X)
⊢ (∃ y_1, ↑f y_1 = ↑(prod.map f g ≫ prod.fst) y) ∧ ∃ y_1, ↑g y_1 = ↑(prod.map f g ≫ prod.snd) y
[PROOFSTEP]
simp only [Limits.prod.map_fst, Limits.prod.map_snd, exists_apply_eq_apply, comp_apply, and_self_iff]
[GOAL]
case h.mpr
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
⊢ x ∈ ↑prod.fst ⁻¹' Set.range ↑f ∩ ↑prod.snd ⁻¹' Set.range ↑g → x ∈ Set.range ↑(prod.map f g)
[PROOFSTEP]
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
[GOAL]
case h.mpr.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ x ∈ Set.range ↑(prod.map f g)
[PROOFSTEP]
use(prodIsoProd W X).inv (x₁, x₂)
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑(prod.map f g) (↑(prodIsoProd W X).inv (x₁, x₂)) = x
[PROOFSTEP]
apply Concrete.limit_ext
[GOAL]
case h.a
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ∀ (j : Discrete WalkingPair),
    ↑(limit.π (pair Y Z) j) (↑(prod.map f g) (↑(prodIsoProd W X).inv (x₁, x₂))) = ↑(limit.π (pair Y Z) j) x
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case h.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑(limit.π (pair Y Z) { as := WalkingPair.left }) (↑(prod.map f g) (↑(prodIsoProd W X).inv (x₁, x₂))) =
    ↑(limit.π (pair Y Z) { as := WalkingPair.left }) x
[PROOFSTEP]
simp only [← comp_apply, Category.assoc]
[GOAL]
case h.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.left }) (x₁, x₂) =
    ↑(limit.π (pair Y Z) { as := WalkingPair.left }) x
[PROOFSTEP]
erw [Limits.prod.map_fst]
[GOAL]
case h.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑((prodIsoProd W X).inv ≫ prod.fst ≫ f) (x₁, x₂) = ↑(limit.π (pair Y Z) { as := WalkingPair.left }) x
[PROOFSTEP]
rw [TopCat.prodIsoProd_inv_fst_assoc, TopCat.comp_app]
[GOAL]
case h.a.mk.left
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑f (↑prodFst (x₁, x₂)) = ↑(limit.π (pair Y Z) { as := WalkingPair.left }) x
[PROOFSTEP]
exact hx₁
[GOAL]
case h.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑(limit.π (pair Y Z) { as := WalkingPair.right }) (↑(prod.map f g) (↑(prodIsoProd W X).inv (x₁, x₂))) =
    ↑(limit.π (pair Y Z) { as := WalkingPair.right }) x
[PROOFSTEP]
simp only [← comp_apply, Category.assoc]
[GOAL]
case h.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑((prodIsoProd W X).inv ≫ prod.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.right }) (x₁, x₂) =
    ↑(limit.π (pair Y Z) { as := WalkingPair.right }) x
[PROOFSTEP]
erw [Limits.prod.map_snd]
[GOAL]
case h.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑((prodIsoProd W X).inv ≫ prod.snd ≫ g) (x₁, x₂) = ↑(limit.π (pair Y Z) { as := WalkingPair.right }) x
[PROOFSTEP]
rw [TopCat.prodIsoProd_inv_snd_assoc, TopCat.comp_app]
[GOAL]
case h.a.mk.right
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (forget TopCat).obj (Y ⨯ Z)
x₁ : (forget TopCat).obj W
hx₁ : ↑f x₁ = ↑prod.fst x
x₂ : (forget TopCat).obj X
hx₂ : ↑g x₂ = ↑prod.snd x
⊢ ↑g (↑prodSnd (x₁, x₂)) = ↑(limit.π (pair Y Z) { as := WalkingPair.right }) x
[PROOFSTEP]
exact hx₂
[GOAL]
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ↑f
hg : Inducing ↑g
⊢ Inducing ↑(prod.map f g)
[PROOFSTEP]
constructor
[GOAL]
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ↑f
hg : Inducing ↑g
⊢ topologicalSpace_forget (W ⨯ Y) = induced (↑(prod.map f g)) (topologicalSpace_forget (X ⨯ Z))
[PROOFSTEP]
simp only [prod_topology, induced_compose, ← coe_comp, Limits.prod.map_fst, Limits.prod.map_snd, induced_inf]
[GOAL]
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ↑f
hg : Inducing ↑g
⊢ induced (↑prod.fst) W.str ⊓ induced (↑prod.snd) Y.str =
    induced (↑(prod.fst ≫ f)) X.str ⊓ induced (↑(prod.snd ≫ g)) Z.str
[PROOFSTEP]
simp only [coe_comp]
[GOAL]
case induced
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Inducing ↑f
hg : Inducing ↑g
⊢ induced (↑prod.fst) W.str ⊓ induced (↑prod.snd) Y.str =
    induced (↑f ∘ ↑prod.fst) X.str ⊓ induced (↑g ∘ ↑prod.snd) Z.str
[PROOFSTEP]
rw [← @induced_compose _ _ _ _ _ f, ← @induced_compose _ _ _ _ _ g, ← hf.induced, ← hg.induced]
[GOAL]
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ↑f
hg : Embedding ↑g
⊢ Function.Injective ↑(prod.map f g)
[PROOFSTEP]
haveI := (TopCat.mono_iff_injective _).mpr hf.inj
[GOAL]
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ↑f
hg : Embedding ↑g
this : Mono f
⊢ Function.Injective ↑(prod.map f g)
[PROOFSTEP]
haveI := (TopCat.mono_iff_injective _).mpr hg.inj
[GOAL]
J : Type v
inst✝ : SmallCategory J
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : Embedding ↑f
hg : Embedding ↑g
this✝ : Mono f
this : Mono g
⊢ Function.Injective ↑(prod.map f g)
[PROOFSTEP]
exact (TopCat.mono_iff_injective _).mp inferInstance
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ Continuous Sum.inl
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ Continuous Sum.inr
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ IsColimit (TopCat.binaryCofan X Y)
[PROOFSTEP]
refine' Limits.BinaryCofan.isColimitMk (fun s => { toFun := Sum.elim s.inl s.inr, continuous_toFun := _ }) _ _ _
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
⊢ Continuous (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))
[PROOFSTEP]
apply Continuous.sum_elim (BinaryCofan.inl s).continuous_toFun (BinaryCofan.inr s).continuous_toFun
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ContinuousMap.mk Sum.inl ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s =
      BinaryCofan.inl s
[PROOFSTEP]
intro s
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
⊢ ContinuousMap.mk Sum.inl ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s =
    BinaryCofan.inl s
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
x✝ : (forget TopCat).obj X
⊢ ↑(ContinuousMap.mk Sum.inl ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s) x✝ =
    ↑(BinaryCofan.inl s) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y),
    ContinuousMap.mk Sum.inr ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s =
      BinaryCofan.inr s
[PROOFSTEP]
intro s
[GOAL]
case refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
⊢ ContinuousMap.mk Sum.inr ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s =
    BinaryCofan.inr s
[PROOFSTEP]
ext
[GOAL]
case refine'_3.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
x✝ : (forget TopCat).obj Y
⊢ ↑(ContinuousMap.mk Sum.inr ≫ (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s) x✝ =
    ↑(BinaryCofan.inr s) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
⊢ ∀ (s : BinaryCofan X Y) (m : of (↑X ⊕ ↑Y) ⟶ s.pt),
    ContinuousMap.mk Sum.inl ≫ m = BinaryCofan.inl s →
      ContinuousMap.mk Sum.inr ≫ m = BinaryCofan.inr s →
        m = (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s
[PROOFSTEP]
intro s m h₁ h₂
[GOAL]
case refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ContinuousMap.mk Sum.inl ≫ m = BinaryCofan.inl s
h₂ : ContinuousMap.mk Sum.inr ≫ m = BinaryCofan.inr s
⊢ m = (fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s
[PROOFSTEP]
ext (x | x)
[GOAL]
case refine'_4.w.inl
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ContinuousMap.mk Sum.inl ≫ m = BinaryCofan.inl s
h₂ : ContinuousMap.mk Sum.inr ≫ m = BinaryCofan.inr s
x : ↑X
⊢ ↑m (Sum.inl x) = ↑((fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s) (Sum.inl x)
case refine'_4.w.inr
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
s : BinaryCofan X Y
m : of (↑X ⊕ ↑Y) ⟶ s.pt
h₁ : ContinuousMap.mk Sum.inl ≫ m = BinaryCofan.inl s
h₂ : ContinuousMap.mk Sum.inr ≫ m = BinaryCofan.inr s
x : ↑Y
⊢ ↑m (Sum.inr x) = ↑((fun s => ContinuousMap.mk (Sum.elim ↑(BinaryCofan.inl s) ↑(BinaryCofan.inr s))) s) (Sum.inr x)
[PROOFSTEP]
exacts [(ConcreteCategory.congr_hom h₁ x : _), (ConcreteCategory.congr_hom h₂ x : _)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    OpenEmbedding ↑(BinaryCofan.inl c) ∧
      OpenEmbedding ↑(BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
[PROOFSTEP]
classical
constructor
· rintro ⟨h⟩
  rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.left⟩, ←
    show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.right⟩]
  dsimp
  refine'
    ⟨(homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inl,
      (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inr,
      _⟩
  erw [Set.range_comp, ← eq_compl_iff_isCompl, coe_comp, coe_comp, Set.range_comp _ Sum.inr, ←
    Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.bijective,
    Set.compl_range_inr, Set.image_comp]
  aesop
· rintro ⟨h₁, h₂, h₃⟩
  have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr :=
    by
    rw [eq_compl_iff_isCompl.mpr h₃.symm]
    exact fun _ => or_not
  refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
  · intro T f g
    refine' ContinuousMap.mk _ _
    ·
      exact fun x =>
        if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁.inj).symm ⟨x, h⟩)
        else g ((Equiv.ofInjective _ h₂.inj).symm ⟨x, (this x).resolve_left h⟩)
    rw [continuous_iff_continuousAt]
    intro x
    by_cases x ∈ Set.range c.inl
    · revert h x
      apply (IsOpen.continuousOn_iff _).mp
      · rw [continuousOn_iff_continuous_restrict]
        convert_to Continuous (f ∘ (Homeomorph.ofEmbedding _ h₁.toEmbedding).symm)
        · ext ⟨x, hx⟩
          exact dif_pos hx
        apply Continuous.comp
        · exact f.continuous_toFun
        · continuity
      · exact h₁.open_range
    · revert h x
      apply (IsOpen.continuousOn_iff _).mp
      · rw [continuousOn_iff_continuous_restrict]
        have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr :=
          by
          rintro a (h : a ∈ (Set.range c.inl)ᶜ)
          rwa [eq_compl_iff_isCompl.mpr h₃.symm]
        convert_to Continuous (g ∘ (Homeomorph.ofEmbedding _ h₂.toEmbedding).symm ∘ Subtype.map _ this)
        · ext ⟨x, hx⟩
          exact dif_neg hx
        apply Continuous.comp
        · exact g.continuous_toFun
        · apply Continuous.comp
          · continuity
          · rw [embedding_subtype_val.toInducing.continuous_iff]
            exact continuous_subtype_val
      · change IsOpen (Set.range c.inl)ᶜ
        rw [← eq_compl_iff_isCompl.mpr h₃.symm]
        exact h₂.open_range
  · intro T f g
    ext x
    refine' (dif_pos _).trans _
    · exact ⟨x, rfl⟩
    · dsimp; conv_lhs => erw [Equiv.ofInjective_symm_apply]
  · intro T f g
    ext x
    refine' (dif_neg _).trans _
    · rintro ⟨y, e⟩
      have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
      rwa [disjoint_iff.mp h₃.1] at this 
    · exact congr_arg g (Equiv.ofInjective_symm_apply _ _)
  · rintro T _ _ m rfl rfl
    ext x
    change m x = dite _ _ _
    split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    OpenEmbedding ↑(BinaryCofan.inl c) ∧
      OpenEmbedding ↑(BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
[PROOFSTEP]
constructor
[GOAL]
case mp
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    OpenEmbedding ↑(BinaryCofan.inl c) ∧
      OpenEmbedding ↑(BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding ↑(BinaryCofan.inl c) ∧
    OpenEmbedding ↑(BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
[PROOFSTEP]
rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.left⟩, ←
  show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCofanIsColimit X Y) ⟨WalkingPair.right⟩]
[GOAL]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ↑(NatTrans.app (TopCat.binaryCofan X Y).ι { as := WalkingPair.left } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv) ∧
    OpenEmbedding
        ↑(NatTrans.app (TopCat.binaryCofan X Y).ι { as := WalkingPair.right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          ↑(NatTrans.app (TopCat.binaryCofan X Y).ι { as := WalkingPair.left } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
        (Set.range
          ↑(NatTrans.app (TopCat.binaryCofan X Y).ι { as := WalkingPair.right } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
[PROOFSTEP]
dsimp
[GOAL]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ↑(BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv) ∧
    OpenEmbedding
        ↑(BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          ↑(BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
        (Set.range
          ↑(BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
[PROOFSTEP]
refine'
  ⟨(homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inl,
    (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inr, _⟩
[GOAL]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      ↑(BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
    (Set.range
      ↑(BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
[PROOFSTEP]
erw [Set.range_comp, ← eq_compl_iff_isCompl, coe_comp, coe_comp, Set.range_comp _ Sum.inr, ←
  Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.bijective,
  Set.compl_range_inr, Set.image_comp]
[GOAL]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ ↑(IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv ''
      (↑(BinaryCofan.inl (TopCat.binaryCofan X Y)) '' Set.range fun x => x) =
    ↑(Homeomorph.symm (homeoOfIso (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)))) ''
      Set.range Sum.inl
[PROOFSTEP]
aesop
[GOAL]
case mpr
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ OpenEmbedding ↑(BinaryCofan.inl c) ∧
      OpenEmbedding ↑(BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c)) →
    Nonempty (IsColimit c)
[PROOFSTEP]
rintro ⟨h₁, h₂, h₃⟩
[GOAL]
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
⊢ Nonempty (IsColimit c)
[PROOFSTEP]
have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr :=
  by
  rw [eq_compl_iff_isCompl.mpr h₃.symm]
  exact fun _ => or_not
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
⊢ ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
[PROOFSTEP]
rw [eq_compl_iff_isCompl.mpr h₃.symm]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
⊢ ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ (Set.range ↑(BinaryCofan.inl c))ᶜ
[PROOFSTEP]
exact fun _ => or_not
[GOAL]
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Nonempty (IsColimit c)
[PROOFSTEP]
refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
[GOAL]
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
⊢ {T : TopCat} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
[PROOFSTEP]
intro T f g
[GOAL]
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ c.pt ⟶ T
[PROOFSTEP]
refine' ContinuousMap.mk _ _
[GOAL]
case mpr.intro.intro.refine'_1.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ↑c.pt → ↑T
[PROOFSTEP]
exact fun x =>
  if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁.inj).symm ⟨x, h⟩)
  else g ((Equiv.ofInjective _ h₂.inj).symm ⟨x, (this x).resolve_left h⟩)
[GOAL]
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous fun x =>
    if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
      ↑f
        (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
          { val := x, property := h })
    else
      ↑g
        (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
          { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ContinuousAt
      (fun x =>
        if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
          ↑f
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h })
        else
          ↑g
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      x
[PROOFSTEP]
intro x
[GOAL]
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    x
[PROOFSTEP]
by_cases x ∈ Set.range c.inl
[GOAL]
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    x
[PROOFSTEP]
by_cases x ∈ Set.range c.inl
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : x ∈ Set.range ↑(BinaryCofan.inl c)
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    x
[PROOFSTEP]
revert h x
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    x ∈ Set.range ↑(BinaryCofan.inl c) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
            ↑f
              (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                { val := x, property := h })
          else
            ↑g
              (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
        x
[PROOFSTEP]
apply (IsOpen.continuousOn_iff _).mp
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    (Set.range ↑(BinaryCofan.inl c))
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (Set.range ↑(BinaryCofan.inl c)) fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
[PROOFSTEP]
convert_to Continuous (f ∘ (Homeomorph.ofEmbedding _ h₁.toEmbedding).symm)
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (Set.range ↑(BinaryCofan.inl c)) fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
    ↑f ∘ ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inl c) (_ : Embedding ↑(BinaryCofan.inl c))))
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
e_2✝ : ↑T = (forget TopCat).obj T
x : ↑c.pt
hx : x ∈ Set.range ↑(BinaryCofan.inl c)
⊢ Set.restrict (Set.range ↑(BinaryCofan.inl c))
      (fun x =>
        if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
          ↑f
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h })
        else
          ↑g
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      { val := x, property := hx } =
    (↑f ∘ ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inl c) (_ : Embedding ↑(BinaryCofan.inl c)))))
      { val := x, property := hx }
[PROOFSTEP]
exact dif_pos hx
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (↑f ∘ ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inl c) (_ : Embedding ↑(BinaryCofan.inl c)))))
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case pos.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous ↑f
[PROOFSTEP]
exact f.continuous_toFun
[GOAL]
case pos.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inl c) (_ : Embedding ↑(BinaryCofan.inl c))))
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ↑(BinaryCofan.inl c))
[PROOFSTEP]
exact h₁.open_range
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : ¬x ∈ Set.range ↑(BinaryCofan.inl c)
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    x
[PROOFSTEP]
revert h x
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ¬x ∈ Set.range ↑(BinaryCofan.inl c) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
            ↑f
              (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                { val := x, property := h })
          else
            ↑g
              (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
        x
[PROOFSTEP]
apply (IsOpen.continuousOn_iff _).mp
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
    fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False) fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
[PROOFSTEP]
have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr :=
  by
  rintro a (h : a ∈ (Set.range c.inl)ᶜ)
  rwa [eq_compl_iff_isCompl.mpr h₃.symm]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
[PROOFSTEP]
rintro a (h : a ∈ (Set.range c.inl)ᶜ)
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h : a ∈ (Set.range ↑(BinaryCofan.inl c))ᶜ
⊢ a ∈ Set.range ↑(BinaryCofan.inr c)
[PROOFSTEP]
rwa [eq_compl_iff_isCompl.mpr h₃.symm]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False) fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
[PROOFSTEP]
convert_to Continuous (g ∘ (Homeomorph.ofEmbedding _ h₂.toEmbedding).symm ∘ Subtype.map _ this)
[GOAL]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
e_1✝ : (↑fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False) = { a // ¬a ∈ Set.range ↑(BinaryCofan.inl c) }
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False) fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
    ↑g ∘
      ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inr c) (_ : Embedding ↑(BinaryCofan.inr c)))) ∘
        Subtype.map (fun a => a) this
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
e_1✝ : (↑fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False) = { a // ¬a ∈ Set.range ↑(BinaryCofan.inl c) }
e_2✝ : ↑T = (forget TopCat).obj T
x : ↑c.pt
hx : x ∈ fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False
⊢ Set.restrict (fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False)
      (fun x =>
        if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
          ↑f
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h })
        else
          ↑g
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      { val := x, property := hx } =
    (↑g ∘
        ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inr c) (_ : Embedding ↑(BinaryCofan.inr c)))) ∘
          Subtype.map (fun a => a) this)
      { val := x, property := hx }
[PROOFSTEP]
exact dif_neg hx
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous
    (↑g ∘
      ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inr c) (_ : Embedding ↑(BinaryCofan.inr c)))) ∘
        Subtype.map (fun a => a) this)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case neg.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous ↑g
[PROOFSTEP]
exact g.continuous_toFun
[GOAL]
case neg.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous
    (↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inr c) (_ : Embedding ↑(BinaryCofan.inr c)))) ∘
      Subtype.map (fun a => a) this)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case neg.hf.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous ↑(Homeomorph.symm (Homeomorph.ofEmbedding ↑(BinaryCofan.inr c) (_ : Embedding ↑(BinaryCofan.inr c))))
[PROOFSTEP]
continuity
[GOAL]
case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous (Subtype.map (fun a => a) this)
[PROOFSTEP]
rw [embedding_subtype_val.toInducing.continuous_iff]
[GOAL]
case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀ (a : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    ¬a ∈ Set.range ↑(BinaryCofan.inl c) → a ∈ Set.range ↑(BinaryCofan.inr c)
⊢ Continuous (Subtype.val ∘ Subtype.map (fun a => a) this)
[PROOFSTEP]
exact continuous_subtype_val
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen fun a => a ∈ Set.range ↑(BinaryCofan.inl c) → False
[PROOFSTEP]
change IsOpen (Set.range c.inl)ᶜ
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ↑(BinaryCofan.inl c))ᶜ
[PROOFSTEP]
rw [← eq_compl_iff_isCompl.mpr h₃.symm]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ↑(BinaryCofan.inr c))
[PROOFSTEP]
exact h₂.open_range
[GOAL]
case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inl c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
            ↑f
              (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                { val := x, property := h })
          else
            ↑g
              (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
      f
[PROOFSTEP]
intro T f g
[GOAL]
case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inl c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
          ↑f
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h })
        else
          ↑g
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
    f
[PROOFSTEP]
ext x
[GOAL]
case mpr.intro.intro.refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ ↑(BinaryCofan.inl c ≫
          ContinuousMap.mk fun x =>
            if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
              ↑f
                (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                  { val := x, property := h })
            else
              ↑g
                (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                  { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      x =
    ↑f x
[PROOFSTEP]
refine' (dif_pos _).trans _
[GOAL]
case mpr.intro.intro.refine'_2.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ ↑(BinaryCofan.inl c) x ∈ Set.range ↑(BinaryCofan.inl c)
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (fun h =>
        ↑f
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := ↑(BinaryCofan.inl c) x, property := h }))
      (_ : ∃ y, ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) =
    ↑f x
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ ↑f
      (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
        { val := ↑(BinaryCofan.inl c) x, property := (_ : ∃ y, ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) }) =
    ↑f x
[PROOFSTEP]
conv_lhs => erw [Equiv.ofInjective_symm_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
| ↑f
    (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
      { val := ↑(BinaryCofan.inl c) x, property := (_ : ∃ y, ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) })
[PROOFSTEP]
erw [Equiv.ofInjective_symm_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
| ↑f
    (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
      { val := ↑(BinaryCofan.inl c) x, property := (_ : ∃ y, ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) })
[PROOFSTEP]
erw [Equiv.ofInjective_symm_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
| ↑f
    (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
      { val := ↑(BinaryCofan.inl c) x, property := (_ : ∃ y, ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) })
[PROOFSTEP]
erw [Equiv.ofInjective_symm_apply]
[GOAL]
case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inr c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
            ↑f
              (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                { val := x, property := h })
          else
            ↑g
              (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
      g
[PROOFSTEP]
intro T f g
[GOAL]
case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inr c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
          ↑f
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h })
        else
          ↑g
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })) =
    g
[PROOFSTEP]
ext x
[GOAL]
case mpr.intro.intro.refine'_3.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ ↑(BinaryCofan.inr c ≫
          ContinuousMap.mk fun x =>
            if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
              ↑f
                (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                  { val := x, property := h })
            else
              ↑g
                (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                  { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      x =
    ↑g x
[PROOFSTEP]
refine' (dif_neg _).trans _
[GOAL]
case mpr.intro.intro.refine'_3.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ ¬↑(BinaryCofan.inr c) x ∈ Set.range ↑(BinaryCofan.inl c)
[PROOFSTEP]
rintro ⟨y, e⟩
[GOAL]
case mpr.intro.intro.refine'_3.w.refine'_1.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
y : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
e : ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
⊢ False
[PROOFSTEP]
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
[GOAL]
case mpr.intro.intro.refine'_3.w.refine'_1.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
y : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
e : ↑(BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
this : ↑(BinaryCofan.inr c) x ∈ Set.range ↑(BinaryCofan.inl c) ⊓ Set.range ↑(BinaryCofan.inr c)
⊢ False
[PROOFSTEP]
rwa [disjoint_iff.mp h₃.1] at this 
[GOAL]
case mpr.intro.intro.refine'_3.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ (fun h =>
        ↑g
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := ↑(BinaryCofan.inr c) x,
              property := (_ : ↑(BinaryCofan.inr c) x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      (_ : ↑(BinaryCofan.inr c) x ∈ Set.range ↑(BinaryCofan.inl c) → False) =
    ↑g x
[PROOFSTEP]
exact congr_arg g (Equiv.ofInjective_symm_apply _ _)
[GOAL]
case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
    BinaryCofan.inl c ≫ m = f →
      BinaryCofan.inr c ≫ m = g →
        m =
          ContinuousMap.mk fun x =>
            if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
              ↑f
                (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                  { val := x, property := h })
            else
              ↑g
                (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                  { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })
[PROOFSTEP]
rintro T _ _ m rfl rfl
[GOAL]
case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
m : c.pt ⟶ T
⊢ m =
    ContinuousMap.mk fun x =>
      if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
        ↑(BinaryCofan.inl c ≫ m)
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h })
      else
        ↑(BinaryCofan.inr c ≫ m)
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) })
[PROOFSTEP]
ext x
[GOAL]
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ ↑m x =
    ↑(ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
            ↑(BinaryCofan.inl c ≫ m)
              (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
                { val := x, property := h })
          else
            ↑(BinaryCofan.inr c ≫ m)
              (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
                { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      x
[PROOFSTEP]
change m x = dite _ _ _
[GOAL]
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ ↑m x =
    if h : x ∈ Set.range ↑(BinaryCofan.inl c) then
      (fun h =>
          ↑(BinaryCofan.inl c ≫ m)
            (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
              { val := x, property := h }))
        h
    else
      (fun h =>
          ↑(BinaryCofan.inr c ≫ m)
            (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
              { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
        h
[PROOFSTEP]
split_ifs
[GOAL]
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
h✝ : x ∈ Set.range ↑(BinaryCofan.inl c)
⊢ ↑m x =
    (fun h =>
        ↑(BinaryCofan.inl c ≫ m)
          (↑(Equiv.ofInjective ↑(BinaryCofan.inl c) (_ : Function.Injective ↑(BinaryCofan.inl c))).symm
            { val := x, property := h }))
      h✝
[PROOFSTEP]
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ↑(BinaryCofan.inl c)
h₂ : OpenEmbedding ↑(BinaryCofan.inr c)
h₃ : IsCompl (Set.range ↑(BinaryCofan.inl c)) (Set.range ↑(BinaryCofan.inr c))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ↑(BinaryCofan.inl c) ∨ x ∈ Set.range ↑(BinaryCofan.inr c)
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
h✝ : ¬x ∈ Set.range ↑(BinaryCofan.inl c)
⊢ ↑m x =
    (fun h =>
        ↑(BinaryCofan.inr c ≫ m)
          (↑(Equiv.ofInjective ↑(BinaryCofan.inr c) (_ : Function.Injective ↑(BinaryCofan.inr c))).symm
            { val := x, property := (_ : x ∈ Set.range ↑(BinaryCofan.inr c)) }))
      h✝
[PROOFSTEP]
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
