-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
⊢ IsColimit (F :=
    pair
      (TopCat.of
        { p :
          (↑Z : Type u) ×
            (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u) //
          Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f :
                  (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                p.1 :
              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) (X :=
                      Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.left : Discrete WalkingPair })
                      (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                      (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                        Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair } ⟶
                          Functor.obj
                            (Functor.obj (Functor.const (Discrete WalkingPair))
                              (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                    C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u),
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                  (a :
                      (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.left }) :
                        Type u)) →
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                p.2 :
              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
      (TopCat.of
        { p :
          (↑Z : Type u) ×
            (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u) //
          Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f :
                  (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                p.1 :
              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) (X :=
                      Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.right : Discrete WalkingPair })
                      (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                      (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                        Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair } ⟶
                          Functor.obj
                            (Functor.obj (Functor.const (Discrete WalkingPair))
                              (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                            { as := WalkingPair.right : Discrete WalkingPair }) :
                    C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair }) :
                        Type u),
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                  (a :
                      (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.right }) :
                        Type u)) →
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                p.2 :
              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
    (BinaryCofan.mk
      (TopCat.pullbackFst f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
      (TopCat.pullbackFst f (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))
have h₁ : Eq (α := Set (↑Z : Type u))
  (Set.range (ι :=
    (↑(TopCat.of
          { p :
            (↑Z : Type u) ×
              (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u) //
            Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f :
                    (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  p.1 :
                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
              (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (X :=
                        Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                          { as := WalkingPair.left : Discrete WalkingPair })
                        (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                        (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                          Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.left : Discrete WalkingPair } ⟶
                            Functor.obj
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                      C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u),
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                    (a :
                        (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.left }) :
                          Type u)) →
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  p.2 :
                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X :=
          TopCat.of
            { p :
              (↑Z : Type u) ×
                (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                      { as := WalkingPair.left : Discrete WalkingPair }) :
                  Type u) //
              Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.1 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (X :=
                          Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair })
                          (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                          (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair } ⟶
                              Functor.obj
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                { as := WalkingPair.left : Discrete WalkingPair }) :
                        C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair }) :
                            Type u),
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                      (a :
                          (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                { as := WalkingPair.left }) :
                            Type u)) →
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.2 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
          (TopCat.pullbackFst f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))) :
      (a :
          (↑(TopCat.of
                { p :
                  (↑Z : Type u) ×
                    (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.left }) :
                      Type u) //
                  (ConcreteCategory.hom f :
                        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.1 =
                    (ConcreteCategory.hom ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl :
                        (a :
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.left }) :
                              Type u)) →
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.2 }) :
            Type u)) →
        (↑Z : Type u)))
  (Set.preimage (β := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
    (Set.range Sum.inl))
Tactic: have h₁ : Set.range (TopCat.pullbackFst f (TopCat.binaryCofan (.of PUnit) (.of PUnit)).inl) =
      f ⁻¹' Set.range Sum.inl := by
    apply le_antisymm
    · rintro _ ⟨x, rfl⟩; exact ⟨PUnit.unit, x.2.symm⟩
    · rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩