Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.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),
    c.inl ≫
        ofHom
          {
            toFun := 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, ⋯⟩),
            continuous_toFun := ⋯ } =
      f

pp: case mpr.refine_3
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.inr ≫
        ofHom
          {
            toFun := 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, ⋯⟩),
            continuous_toFun := ⋯ } =
      g

pp: case mpr.refine_4
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) (m : c.pt ⟶ T),
    c.inl ≫ m = f →
      c.inr ≫ m = g →
        m =
          ofHom
            {
              toFun := 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, ⋯⟩),
              continuous_toFun := ⋯ }

Tactic:
· intro T f g
        ext x
        simp

Goal state after:
case mpr.refine_3
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.inr ≫
        ofHom
          {
            toFun := 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, ⋯⟩),
            continuous_toFun := ⋯ } =
      g

case mpr.refine_4
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) (m : c.pt ⟶ T),
    c.inl ≫ m = f →
      c.inr ≫ m = g →
        m =
          ofHom
            {
              toFun := 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, ⋯⟩),
              continuous_toFun := ⋯ }