-- 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
h :
  ∀ (x_3 : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj x),
    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
⊢ (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 := ⋯ }) =
    (↾fun (x_3 : 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_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.toTopCat : Type u)) }) ≫
      X.toTopCat.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map x_2

Tactic:
ext