-- 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 mpr.intro.intro.refine_2.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
f : X ⟶ T
g : Y ⟶ T
x : ↑((pair X Y).obj { as := WalkingPair.left })
⊢ (if h : (Hom.hom c.inl) x ∈ range ⇑(ConcreteCategory.hom c.inl) then
      (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨(Hom.hom c.inl) x, h⟩)
    else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨(Hom.hom c.inl) x, ⋯⟩)) =
    (ConcreteCategory.hom f) x

Tactic:
rw [dif_pos]

Result:
case mpr.intro.intro.refine_2.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
f : X ⟶ T
g : Y ⟶ T
x : ↑((pair X Y).obj { as := WalkingPair.left })
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨(Hom.hom c.inl) x, ?mpr.intro.intro.refine_2.w.hc⟩) =
    (ConcreteCategory.hom f) x

case mpr.intro.intro.refine_2.w.hc
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
x : ↑((pair X Y).obj { as := WalkingPair.left })
⊢ (Hom.hom c.inl) x ∈ range ⇑(ConcreteCategory.hom c.inl)

Proof state:
case mpr.intro.intro.refine_1
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
⊢ c.pt ⟶ T

Tactic:
refine ofHom (ContinuousMap.mk ?_ ?_)

Result:
case mpr.intro.intro.refine_1.refine_1
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
⊢ ↑c.1 → ↑T

case mpr.intro.intro.refine_1.refine_2
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 ?mpr.intro.intro.refine_1.refine_1

Proof state:
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
⊢ ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)

Tactic:
rintro a (h : a ∈ (Set.range c.inl)ᶜ)

Result:
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
a : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h : a ∈ (range ⇑(ConcreteCategory.hom c.inl))ᶜ
⊢ a ∈ range ⇑(ConcreteCategory.hom c.inr)

Proof state:
case neg.hf.hf
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
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (Subtype.val ∘ Subtype.map (fun a => a) this)

Tactic:
exact continuous_subtype_val

Result:
no goals