-- 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
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))

Tactic:
ConcreteCategory.congr_hom h₂ _

Premises used: CategoryTheory.ConcreteCategory.congr_hom, Sum.elim