case mp
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
      OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
        IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
          (Set.range ((forget TopCat).map (BinaryCofan.inr c)))

case mpr
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
      OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
        IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
          (Set.range ((forget TopCat).map (BinaryCofan.inr c))) →
    Nonempty (IsColimit c)
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
      OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
        IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
          (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
constructor
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
    OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
      IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
        (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
case mp
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
      OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
        IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
          (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
rintro ⟨h⟩
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ((forget TopCat).map
        ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.left } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
    OpenEmbedding
        ((forget TopCat).map
          ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ((forget TopCat).map
            ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.left } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
        (Set.range
          ((forget TopCat).map
            ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.right } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
    OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
      IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
        (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
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⟩]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ((forget TopCat).map
        (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
    OpenEmbedding
        ((forget TopCat).map
          (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ((forget TopCat).map
            (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
        (Set.range
          ((forget TopCat).map
            (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ((forget TopCat).map
        ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.left } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
    OpenEmbedding
        ((forget TopCat).map
          ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ((forget TopCat).map
            ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.left } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
        (Set.range
          ((forget TopCat).map
            ((TopCat.binaryCofan X Y).ι.app { as := WalkingPair.right } ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
dsimp
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      ((forget TopCat).map
        (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
    (Set.range
      ((forget TopCat).map
        (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ OpenEmbedding
      ((forget TopCat).map
        (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
    OpenEmbedding
        ((forget TopCat).map
          (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ((forget TopCat).map
            (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
        (Set.range
          ((forget TopCat).map
            (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
              (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
refine' ⟨(homeoOfIso <| h.coconePointUniqueUpToIso
  (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inl,
    (homeoOfIso <| h.coconePointUniqueUpToIso
      (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inr, _⟩
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      ((forget TopCat).map (BinaryCofan.inl (TopCat.binaryCofan X Y)) ≫
        (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
    (Set.range
      ((forget TopCat).map (BinaryCofan.inr (TopCat.binaryCofan X Y)) ≫
        (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      ((forget TopCat).map
        (BinaryCofan.inl (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
    (Set.range
      ((forget TopCat).map
        (BinaryCofan.inr (TopCat.binaryCofan X Y) ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv)))
simp only [Functor.map_comp]
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv '' Set.range Sum.inrᶜ =
    ↑(Homeomorph.symm (homeoOfIso (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)))) ''
      Set.range Sum.inrᶜ
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (Set.range
      ((forget TopCat).map (BinaryCofan.inl (TopCat.binaryCofan X Y)) ≫
        (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
    (Set.range
      ((forget TopCat).map (BinaryCofan.inr (TopCat.binaryCofan X Y)) ≫
        (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv))
erw [Set.range_comp, ← eq_compl_iff_isCompl, Set.range_comp _ Sum.inr,
  ← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
    (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr.symm]
no goals
case mp.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ (forget TopCat).map (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)).inv '' Set.range Sum.inrᶜ =
    ↑(Homeomorph.symm (homeoOfIso (IsColimit.coconePointUniqueUpToIso h (binaryCofanIsColimit X Y)))) ''
      Set.range Sum.inrᶜ
congr 1
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
⊢ Nonempty (IsColimit c)
case mpr
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
⊢ OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c)) ∧
      OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c)) ∧
        IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
          (Set.range ((forget TopCat).map (BinaryCofan.inr c))) →
    Nonempty (IsColimit c)
rintro ⟨h₁, h₂, h₃⟩
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Nonempty (IsColimit c)
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
⊢ Nonempty (IsColimit c)
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
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ {T : TopCat} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T), BinaryCofan.inl c ≫ ?mpr.intro.intro.refine'_1 f g = f

case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T), BinaryCofan.inr c ≫ ?mpr.intro.intro.refine'_1 f g = g

case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 = ?mpr.intro.intro.refine'_1 f g
case mpr.intro.intro
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Nonempty (IsColimit c)
refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
⊢ ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))ᶜ
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
⊢ ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
rw [eq_compl_iff_isCompl.mpr h₃.symm]
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
⊢ ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))ᶜ
exact fun _ => or_not
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ c.pt ⟶ T
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ {T : TopCat} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
intro T f g
case mpr.intro.intro.refine'_1.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ↑c.pt → ↑T

case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous ?mpr.intro.intro.refine'_1.refine'_1
case mpr.intro.intro.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ c.pt ⟶ T
refine' ContinuousMap.mk _ _
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ContinuousAt
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous fun x =>
    if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
      (forget TopCat).map f
        (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
          { val := x, property := h })
    else
      (forget TopCat).map g
        (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
          { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })
rw [continuous_iff_continuousAt]
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ContinuousAt
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x
intro x
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x

case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : ¬x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x
case mpr.intro.intro.refine'_1.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x
by_cases x ∈ Set.range c.inl
no goals
case mpr.intro.intro.refine'_1.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ↑c.pt → ↑T
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⟩)
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        x
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x
revert h x
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    (Set.range ((forget TopCat).map (BinaryCofan.inl c)))

J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        x
apply (IsOpen.continuousOn_iff _).mp
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c))) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
rw [continuousOn_iff_continuous_restrict]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c))) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    (forget TopCat).map f ∘
      ↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c)))))

case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ((forget TopCat).map f ∘
      ↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c))))))
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c))) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
convert_to Continuous (f ∘ (Homeomorph.ofEmbedding _ h₁.toEmbedding).symm)
case pos.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous ((forget TopCat).map f)

case pos.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ↑(Homeomorph.symm
        (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
          (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c)))))
case pos
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ((forget TopCat).map f ∘
      ↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c))))))
apply Continuous.comp
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))
⊢ Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      { val := x, property := hx } =
    ((forget TopCat).map f ∘
        ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c))))))
      { val := x, property := hx }
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c))) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    (forget TopCat).map f ∘
      ↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c)))))
ext ⟨x, hx⟩
no goals
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))
⊢ Set.restrict (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      { val := x, property := hx } =
    ((forget TopCat).map f ∘
        ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c))))))
      { val := x, property := hx }
exact dif_pos hx
no goals
case pos.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous ((forget TopCat).map f)
exact f.continuous_toFun
no goals
case pos.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ↑(Homeomorph.symm
        (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inl c))
          (_ : Embedding ((forget TopCat).map (BinaryCofan.inl c)))))
continuity
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inl c)))
exact h₁.open_range
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ¬x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        x
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑c.pt
h : ¬x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c))
⊢ ContinuousAt
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    x
revert h x
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False

J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ∀ (x : ↑c.pt),
    ¬x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) →
      ContinuousAt
        (fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        x
apply (IsOpen.continuousOn_iff _).mp
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
    fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False
rw [continuousOn_iff_continuous_restrict]
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
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]
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
e_1✝ :
  (↑fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) =
    { a // ¬a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) }
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    (forget TopCat).map g ∘
      ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
        Subtype.map (fun a => a) this

case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    ((forget TopCat).map g ∘
      ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
        Subtype.map (fun a => a) this)
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
convert_to Continuous
    (g ∘ (Homeomorph.ofEmbedding _ h₂.toEmbedding).symm ∘ Subtype.map _ this)
case neg.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous ((forget TopCat).map g)

case neg.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    (↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
      Subtype.map (fun a => a) this)
case neg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    ((forget TopCat).map g ∘
      ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
        Subtype.map (fun a => a) this)
apply Continuous.comp
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))ᶜ
⊢ a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
rintro a (h : a ∈ Set.range c.inlᶜ)
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))ᶜ
⊢ a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
rwa [eq_compl_iff_isCompl.mpr h₃.symm]
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
e_1✝ :
  (↑fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) =
    { a // ¬a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) }
e_2✝ : ↑T = (forget TopCat).obj T
x : ↑c.pt
hx : x ∈ fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False
⊢ Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False)
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      { val := x, property := hx } =
    ((forget TopCat).map g ∘
        ↑(Homeomorph.symm
              (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
                (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
          Subtype.map (fun a => a) this)
      { val := x, property := hx }
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
e_1✝ :
  (↑fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) =
    { a // ¬a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) }
e_2✝ : ↑T = (forget TopCat).obj T
⊢ (Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    (forget TopCat).map g ∘
      ↑(Homeomorph.symm
            (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
              (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
        Subtype.map (fun a => a) this
ext ⟨x, hx⟩
no goals
case h.e'_5.h.h.mk
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
e_1✝ :
  (↑fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) =
    { a // ¬a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) }
e_2✝ : ↑T = (forget TopCat).obj T
x : ↑c.pt
hx : x ∈ fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False
⊢ Set.restrict (fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False)
      (fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      { val := x, property := hx } =
    ((forget TopCat).map g ∘
        ↑(Homeomorph.symm
              (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
                (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
          Subtype.map (fun a => a) this)
      { val := x, property := hx }
exact dif_neg hx
no goals
case neg.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous ((forget TopCat).map g)
exact g.continuous_toFun
case neg.hf.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    ↑(Homeomorph.symm
        (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
          (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c)))))

case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous (Subtype.map (fun a => a) this)
case neg.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    (↑(Homeomorph.symm
          (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
            (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c))))) ∘
      Subtype.map (fun a => a) this)
apply Continuous.comp
no goals
case neg.hf.hg
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous
    ↑(Homeomorph.symm
        (Homeomorph.ofEmbedding ((forget TopCat).map (BinaryCofan.inr c))
          (_ : Embedding ((forget TopCat).map (BinaryCofan.inr c)))))
continuity
case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous (Subtype.val ∘ Subtype.map (fun a => a) this)
case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous (Subtype.map (fun a => a) this)
rw [embedding_subtype_val.toInducing.continuous_iff]
no goals
case neg.hf.hf
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) → a ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ Continuous (Subtype.val ∘ Subtype.map (fun a => a) this)
exact continuous_subtype_val
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inl c))ᶜ)
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen fun a => a ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False
change IsOpen (Set.range c.inlᶜ)
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inl c))ᶜ)
rw [← eq_compl_iff_isCompl.mpr h₃.symm]
no goals
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ IsOpen (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
exact h₂.open_range
case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inl c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    f
case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inl c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
      f
intro T f g
case mpr.intro.intro.refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (forget TopCat).map
      (BinaryCofan.inl c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x =
    (forget TopCat).map f x
case mpr.intro.intro.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inl c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    f
ext x
case mpr.intro.intro.refine'_2.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))

case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (fun h =>
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := ↑(BinaryCofan.inl c) x, property := h }))
      ?mpr.intro.intro.refine'_2.w.refine'_1 =
    (forget TopCat).map f x
case mpr.intro.intro.refine'_2.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (forget TopCat).map
      (BinaryCofan.inl c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x =
    (forget TopCat).map f x
refine' (dif_pos _).trans _
no goals
case mpr.intro.intro.refine'_2.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))
exact ⟨x, rfl⟩
case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (forget TopCat).map f
      (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
              (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
        { val := ↑(BinaryCofan.inl c) x,
          property := (_ : ∃ y, (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) }) =
    (forget TopCat).map f x
case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (fun h =>
        (forget TopCat).map f
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := ↑(BinaryCofan.inl c) x, property := h }))
      (_ : ∃ y, (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) =
    (forget TopCat).map f x
dsimp
no goals
case mpr.intro.intro.refine'_2.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.left })
⊢ (forget TopCat).map f
      (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
              (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
        { val := ↑(BinaryCofan.inl c) x,
          property := (_ : ∃ y, (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inl c) x) }) =
    (forget TopCat).map f x
conv_lhs => erw [Equiv.ofInjective_symm_apply]
case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inr c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    g
case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inr c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
      g
intro T f g
case mpr.intro.intro.refine'_3.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ (forget TopCat).map
      (BinaryCofan.inr c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x =
    (forget TopCat).map g x
case mpr.intro.intro.refine'_3
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inr c ≫
      ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map f
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map g
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })) =
    g
ext x
case mpr.intro.intro.refine'_3.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))

case mpr.intro.intro.refine'_3.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ (fun h =>
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := ↑(BinaryCofan.inr c) x,
              property := (_ : ↑(BinaryCofan.inr c) x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      ?mpr.intro.intro.refine'_3.w.refine'_1 =
    (forget TopCat).map g x
case mpr.intro.intro.refine'_3.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ (forget TopCat).map
      (BinaryCofan.inr c ≫
        ContinuousMap.mk fun x =>
          if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
            (forget TopCat).map f
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                { val := x, property := h })
          else
            (forget TopCat).map g
              (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                      (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x =
    (forget TopCat).map g x
refine' (dif_neg _).trans _
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 ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 : (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
⊢ False
case mpr.intro.intro.refine'_3.w.refine'_1
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c))
rintro ⟨y, e⟩
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 ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 : (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
this :
  (forget TopCat).map (BinaryCofan.inr c) x ∈
    Set.range ((forget TopCat).map (BinaryCofan.inl c)) ⊓ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ False
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 ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 : (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
⊢ False
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
no goals
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 ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this✝ :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 : (forget TopCat).map (BinaryCofan.inl c) y = ↑(BinaryCofan.inr c) x
this :
  (forget TopCat).map (BinaryCofan.inr c) x ∈
    Set.range ((forget TopCat).map (BinaryCofan.inl c)) ⊓ Set.range ((forget TopCat).map (BinaryCofan.inr c))
⊢ False
rwa [disjoint_iff.mp h₃.1] at this
no goals
case mpr.intro.intro.refine'_3.w.refine'_2
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : (forget TopCat).obj ((pair X Y).obj { as := WalkingPair.right })
⊢ (fun h =>
        (forget TopCat).map g
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := ↑(BinaryCofan.inr c) x,
              property := (_ : ↑(BinaryCofan.inr c) x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      (_ : ↑(BinaryCofan.inr c) x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) → False) =
    (forget TopCat).map g x
exact congr_arg g (Equiv.ofInjective_symm_apply _ _)
case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
⊢ m =
    ContinuousMap.mk fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map (BinaryCofan.inl c ≫ m)
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map (BinaryCofan.inr c ≫ m)
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })
case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (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 ((forget TopCat).map (BinaryCofan.inl c)) then
              (forget TopCat).map f
                (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                        (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
                  { val := x, property := h })
            else
              (forget TopCat).map g
                (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                        (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
                  { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })
rintro T _ _ m rfl rfl
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ (forget TopCat).map m x =
    (forget TopCat).map
      (ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map (BinaryCofan.inl c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map (BinaryCofan.inr c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x
case mpr.intro.intro.refine'_4
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
⊢ m =
    ContinuousMap.mk fun x =>
      if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
        (forget TopCat).map (BinaryCofan.inl c ≫ m)
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
            { val := x, property := h })
      else
        (forget TopCat).map (BinaryCofan.inr c ≫ m)
          (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                  (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
            { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) })
ext x
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ (forget TopCat).map m x =
    if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
      (fun h =>
          (forget TopCat).map (BinaryCofan.inl c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h }))
        h
    else
      (fun h =>
          (forget TopCat).map (BinaryCofan.inr c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        h
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ (forget TopCat).map m x =
    (forget TopCat).map
      (ContinuousMap.mk fun x =>
        if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
          (forget TopCat).map (BinaryCofan.inl c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h })
        else
          (forget TopCat).map (BinaryCofan.inr c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
      x
change m x = dite _ _ _
no goals
case mpr.intro.intro.refine'_4.w
J : Type v
inst✝ : SmallCategory J
X Y : TopCat
c : BinaryCofan X Y
h₁ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inl c))
h₂ : OpenEmbedding ((forget TopCat).map (BinaryCofan.inr c))
h₃ : IsCompl (Set.range ((forget TopCat).map (BinaryCofan.inl c))) (Set.range ((forget TopCat).map (BinaryCofan.inr c)))
this :
  ∀ (x : (forget TopCat).obj (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) ∨ x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))
T : TopCat
m : c.pt ⟶ T
x : (forget TopCat).obj c.pt
⊢ (forget TopCat).map m x =
    if h : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inl c)) then
      (fun h =>
          (forget TopCat).map (BinaryCofan.inl c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inl c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inl c)))).symm
              { val := x, property := h }))
        h
    else
      (fun h =>
          (forget TopCat).map (BinaryCofan.inr c ≫ m)
            (↑(Equiv.ofInjective ((forget TopCat).map (BinaryCofan.inr c))
                    (_ : Function.Injective ((forget TopCat).map (BinaryCofan.inr c)))).symm
              { val := x, property := (_ : x ∈ Set.range ((forget TopCat).map (BinaryCofan.inr c))) }))
        h
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm