-- Module: Mathlib.Topology.Category.CompHausLike.Cartesian
Goal:
P : TopCat.{u} → Prop
X Y : CompHausLike P
inst : HasProp P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u))
x : BinaryCofan X Y
x_1 : of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ x.pt
h₁ : ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ x_1 = x.inl
h₂ : ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ x_1 = x.inr
h :
  ∀ (val : (↑(X.toTop (P := P)) : Type u)),
    Eq (α := (↑(x.pt.toTop (P := P)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) x_1 :
            (a : (↑(of P ((↑X.toTop : Type u) ⊕ (↑Y.toTop : Type u))).toTop : Type u)) → (↑x.pt.toTop : Type u))
          (Sum.inl val) :
        (↑(x.pt.toTop (P := P)) : Type u))
      ((@ConcreteCategory.hom _ (category P)
              (fun (x1 x2 : CompHausLike P) ↦ C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u)))
              (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) _ _
              (of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u))) x.pt
              ((fun (s : BinaryCofan X Y) ↦
                  (ofHom P
                      {
                        toFun :=
                          Sum.elim
                            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                                  C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                                  fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inl) :
                              (a :
                                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                    ((pair X Y).obj { as := WalkingPair.left })) →
                                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                                  C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                                  fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inr) :
                              (a :
                                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                    ((pair X Y).obj { as := WalkingPair.right })) →
                                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })),
                        continuous_toFun := ⋯ } :
                    of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ of P (↑s.1.1 : Type u)))
                x) :
            (a : (↑(of P ((↑X.toTop : Type u) ⊕ (↑Y.toTop : Type u))).toTop : Type u)) → (↑x.pt.toTop : Type u))
          (Sum.inl val) :
        (↑(x.pt.toTop (P := P)) : Type u))
h₃ :
  ∀ (val : (↑(Y.toTop (P := P)) : Type u)),
    Eq (α := (↑(x.pt.toTop (P := P)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) x_1 :
            (a : (↑(of P ((↑X.toTop : Type u) ⊕ (↑Y.toTop : Type u))).toTop : Type u)) → (↑x.pt.toTop : Type u))
          (Sum.inr val) :
        (↑(x.pt.toTop (P := P)) : Type u))
      ((@ConcreteCategory.hom _ (category P)
              (fun (x1 x2 : CompHausLike P) ↦ C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u)))
              (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) _ _
              (of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u))) x.pt
              ((fun (s : BinaryCofan X Y) ↦
                  (ofHom P
                      {
                        toFun :=
                          Sum.elim
                            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                                  C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                                  fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inl) :
                              (a :
                                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                    ((pair X Y).obj { as := WalkingPair.left })) →
                                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                                  C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                                  fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inr) :
                              (a :
                                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                    ((pair X Y).obj { as := WalkingPair.right })) →
                                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })),
                        continuous_toFun := ⋯ } :
                    of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ of P (↑s.1.1 : Type u)))
                x) :
            (a : (↑(of P ((↑X.toTop : Type u) ⊕ (↑Y.toTop : Type u))).toTop : Type u)) → (↑x.pt.toTop : Type u))
          (Sum.inr val) :
        (↑(x.pt.toTop (P := P)) : Type u))
⊢ x_1 =
    (fun (s : BinaryCofan X Y) ↦
        (ofHom P
            {
              toFun :=
                Sum.elim
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                        C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                        fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inl) :
                    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.left })) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                        C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                        fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) s.inr) :
                    (a :
                        (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) ((pair X Y).obj { as := WalkingPair.right })) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })),
              continuous_toFun := ⋯ } :
          of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)) ⟶ of P (↑s.1.1 : Type u)))
      x

Tactic:
ext ⟨⟩