-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 X : CondensedSet
x x_1 : CompHausᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map x_2 ≫
          ↾fun (x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj x_1) ↦
            {
              toFun :=
                fun
                  (s :
                    (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) :
                      Type u)) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                        (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
                    (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop x_1)))) →
                      (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
                  x,
              continuous_toFun := ⋯ :
              C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) :
                  Type u),
                (↑X.toTopCat : Type (u + 1))) }))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj x) ↦
            {
              toFun :=
                fun
                  (s :
                    (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) :
                      Type u)) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                        (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
                    (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop x)))) →
                      (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
                  x_4,
              continuous_toFun := ⋯ :
              C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) :
                  Type u),
                (↑X.toTopCat : Type (u + 1))) }) ≫
          X.toTopCat.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map x_2))
      x_3
have h : {
    toFun :=
      fun
        (s :
          (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) : Type u)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (x_2 ≫ (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op)) :
          (a : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
        x_3,
    continuous_toFun := sorry :
    C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) : Type u),
      X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) } =
  {
        toFun :=
          fun
            (s :
              (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) :
                Type u)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                  (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
              (a : X.obj.obj (Opposite.op (Opposite.unop x))) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
            x_3,
        continuous_toFun := sorry :
        C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) : Type u),
          X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) }.comp
    (TopCat.Hom.hom x_2.unop.hom)
Tactic: simp only [TopCat.toSheafCompHausLike_obj_obj, TypeCat.Fun.toFun_apply,
        comp_apply, TopCat.toSheafCompHausLike_obj_map, ConcreteCategory.hom_ofHom,
        TypeCat.Fun.coe_mk, ← Functor.map_comp_apply]