-- 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 : BinaryCofan X Y),
    CategoryStruct.comp (Y := of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)))
        (ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ })
        ((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)))
          s) =
      s.inl
⊢ ∀ (s : BinaryCofan X Y),
    CategoryStruct.comp (Y := of P ((↑(X.toTop (P := P)) : Type u) ⊕ (↑(Y.toTop (P := P)) : Type u)))
        (ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ })
        ((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)))
          s) =
      s.inl

Tactic:
rfl_cat