-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔
      IsOpenEmbedding c.inl ∧ IsOpenEmbedding c.inr ∧ IsCompl (range c.inl) (range c.inr)

Proof state:
case neg
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ContinuousOn
    (fun x =>
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))
    fun a => a ∈ range ⇑(ConcreteCategory.hom c.inl) → False

Tactic:
rw [continuousOn_iff_continuous_restrict]

Result:
case neg
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    (restrict (fun a => a ∈ range ⇑(ConcreteCategory.hom c.inl) → False) fun x =>
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))

Proof state:
case mp
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))

Tactic:
rintro ⟨h⟩

Result:
case mp.intro
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))

Proof state:
case mpr.intro.intro.refine_4.w
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
m : c.pt ⟶ T
x : ↑c.pt
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom
        (ofHom
          {
            toFun := fun x =>
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ }))
      x

Tactic:
change m x = dite _ _ _

Result:
case mpr.intro.intro.refine_4.w
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
m : c.pt ⟶ T
x : ↑c.pt
⊢ (ConcreteCategory.hom m) x =
    if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
      (ConcreteCategory.hom (c.inl ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
    else (ConcreteCategory.hom (c.inr ≫ m)) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)

Proof state:
case mp.intro
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inl)) ∧
    IsOpenEmbedding
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inr)) ∧
      IsCompl
        (range
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inl)))
        (range
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inr)))

Tactic:
refine ⟨(homeoOfIso <| h.coconePointUniqueUpToIso
  (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inl,
    (homeoOfIso <| h.coconePointUniqueUpToIso
      (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inr, ?_⟩

Result:
case mp.intro
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (range (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inl)))
    (range (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘ ⇑(Hom.hom (X.binaryCofan Y).inr)))

Proof state:
case pos
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ((range ⇑(ConcreteCategory.hom c.inl)).restrict fun x =>
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))

Tactic:
convert_to Continuous (f ∘ (Homeomorph.ofIsEmbedding _ h₁.isEmbedding).symm)

Result:
case h.e'_5
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ((range ⇑(ConcreteCategory.hom c.inl)).restrict fun x =>
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)) =
    ⇑(ConcreteCategory.hom f) ∘ ⇑(Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom c.inl) ⋯).symm

case pos
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous (⇑(ConcreteCategory.hom f) ∘ ⇑(Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom c.inl) ⋯).symm)