-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
f :
  LocallyConstant
    (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    (X.obj
      (Opposite.op
        (CompHausLike.of
          (fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
          PUnit.{u + 1})))
w :
  ∀
    (a :
      Function.Fiber (Y :=
        (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
        (Z :=
        X.obj
          (Opposite.op
            (CompHausLike.of
              (fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              PUnit.{u + 1})))
        (⇑f :
          (a : (↑(toLightProfinite.obj (Opposite.unop Y)).toTop : Type u)) →
            X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
                  PUnit.{u + 1})))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X.obj
          (Opposite.op
            (fiber (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (sigmaIncl (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f a))) :
            (a_1 : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f a))))
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((↾fun
                    (f :
                      LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
                  (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
                Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y)))))
            f) :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (fiber (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (sigmaIncl (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f a))) :
            (a_1 : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f a))))
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (counitApp (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
                (Opposite.op (toLightProfinite.obj (Opposite.unop Y)))))
            f) :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (fiber (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f a))))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
            (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
          Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y)))))
      f =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
          (Opposite.op (toLightProfinite.obj (Opposite.unop Y)))))
      f

Tactic:
apply presheaf_ext.{u, u} (X := X) (Y := X) (f := f)