-- Module: Mathlib.Condensed.Light.TopCatAdjunction
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
x x_1 : LightProfiniteᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj x
h :
  {
      toFun :=
        fun
          (s :
            (↑(Functor.obj
                  (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (Opposite.unop x_1)) :
              Type u)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (x_2 ≫
                  (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (of PUnit.{u + 1}) s).op)) :
            (a : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x_3,
      continuous_toFun := ⋯ :
      C((↑(Functor.obj
              (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              (Opposite.unop x_1)) :
          Type u),
        X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1}))) } =
    {
          toFun :=
            fun
              (s :
                (↑(Functor.obj
                      (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (Opposite.unop x)) :
                  Type u)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                    (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                        (of PUnit.{u + 1}) s).op) :
                (a : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
              x_3,
          continuous_toFun := ⋯ :
          C((↑(Functor.obj
                  (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  (Opposite.unop x)) :
              Type u),
            X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1}))) }.comp
      (TopCat.Hom.hom x_2.unop.hom)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map x_2 ≫
          ↾fun (x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj x_1) ↦
            {
              toFun :=
                fun
                  (s :
                    (↑(Functor.obj
                          (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                          (Opposite.unop x_1)) :
                      Type u)) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                        (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                            (of PUnit.{u + 1}) s).op) :
                    (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop x_1)))) →
                      (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
                  x,
              continuous_toFun := ⋯ :
              C((↑(Functor.obj
                      (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (Opposite.unop x_1)) :
                  Type u),
                (↑X.toTopCat : Type u)) }))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj x) ↦
            {
              toFun :=
                fun
                  (s :
                    (↑(Functor.obj
                          (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                          (Opposite.unop x)) :
                      Type u)) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                        (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                            (of PUnit.{u + 1}) s).op) :
                    (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop x)))) →
                      (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
                  x_4,
              continuous_toFun := ⋯ :
              C((↑(Functor.obj
                      (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                      (Opposite.unop x)) :
                  Type u),
                (↑X.toTopCat : Type u)) }) ≫
          X.toTopCat.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map x_2))
      x_3

Tactic:
simp only [TopCat.toSheafCompHausLike_obj_obj, Opposite.op_unop, TypeCat.Fun.toFun_apply,
        comp_apply, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        TopCat.toSheafCompHausLike_obj_map, ← Functor.map_comp_apply]

Premises used: Opposite.op_unop, TypeCat.Fun.coe_mk, CategoryTheory.Functor.map_comp_apply, TopCat.toSheafCompHausLike_obj_obj, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, TopCat.toSheafCompHausLike_obj_map, CategoryTheory.ConcreteCategory.hom_ofHom