-- 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))
rfl_cat rfl_cat₁ rfl_cat₂ rfl_cat₃ :
  ∀ (s : BinaryFan X Y),
    CategoryStruct.comp (Y := of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
        ((fun (s : BinaryFan X Y) ↦
            (ofHom P
                {
                  toFun := fun (x : (↑s.1.1 : 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)) s.fst :
                          (a :
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left })) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              ((pair X Y).obj { as := WalkingPair.left }))
                        x,
                      (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.snd :
                          (a :
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              ((pair X Y).obj { as := WalkingPair.right }))
                        x),
                  continuous_toFun := ⋯ } :
              of P (↑s.1.1 : Type u) ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))))
          s)
        (ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ }) =
      s.fst
⊢ ∀ (s : BinaryFan X Y),
    CategoryStruct.comp (Y := of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u)))
        ((fun (s : BinaryFan X Y) ↦
            (ofHom P
                {
                  toFun := fun (x : (↑s.1.1 : 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)) s.fst :
                          (a :
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left })) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              ((pair X Y).obj { as := WalkingPair.left }))
                        x,
                      (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.snd :
                          (a :
                              (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                                (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right })) →
                            (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u))
                              ((pair X Y).obj { as := WalkingPair.right }))
                        x),
                  continuous_toFun := ⋯ } :
              of P (↑s.1.1 : Type u) ⟶ of P ((↑(X.toTop (P := P)) : Type u) × (↑(Y.toTop (P := P)) : Type u))))
          s)
        (ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ }) =
      s.fst

Tactic:
rfl_cat