-- 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})))
x :
  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})))
this :
  Finite.{u + 1}
    (↑((fiber (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
          (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
w :
  ∀
    (y :
      (↑((fiber (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
            (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)),
    Eq (α := X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.hom
                (isoFinYonedaComponents X
                  (fiber (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
              (fun (X : Type u) ↦ X)
                ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          ((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 x))) :
                (a : X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj))) → X.obj (Opposite.op (fiber f x)))
              (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                        (Iso.inv (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj))) :
                      TypeCat.Fun ((Opposite.unop Y).obj → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
                        (X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj)))) :
                    (a : (Opposite.unop Y).obj → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) →
                      X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj)))
                  (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) :
                X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj))) :
            X.obj
              (Opposite.op
                (fiber (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x)))
          y :
        X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.hom
                (isoFinYonedaComponents X
                  (fiber (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
              (fun (X : Type u) ↦ X)
                ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map
                    (Quiver.Hom.op
                      (IsTerminal.from
                        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))
                        (fiber (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f
                          x)))) :
                (a :
                    X.obj
                      (Opposite.op
                        (CompHausLike.of
                          (fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
                          PUnit.{u + 1}))) →
                  X.obj (Opposite.op (fiber f x)))
              (Function.Fiber.image
                (⇑f :
                  (a : (Opposite.unop Y).obj) →
                    X.obj
                      (Opposite.op
                        (CompHausLike.of
                          (fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
                          PUnit.{u + 1})))
                x) :
            X.obj
              (Opposite.op
                (fiber (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x)))
          y :
        X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((↑((fiber (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u) →
        X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
              (isoFinYonedaComponents X
                (fiber (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
            (fun (X : Type u) ↦ X)
              ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        ((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 x))) :
              (a : X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj))) → X.obj (Opposite.op (fiber f x)))
            (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                      (Iso.inv (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj))) :
                    TypeCat.Fun ((Opposite.unop Y).obj → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
                      (X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj)))) :
                  (a : (Opposite.unop Y).obj → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) →
                    X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj)))
                (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) :
              X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj))) :
          X.obj
            (Opposite.op
              (fiber (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
      (fun (X : Type u) ↦ X)
        ((↑((fiber (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u) →
          X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
              (isoFinYonedaComponents X
                (fiber (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
            (fun (X : Type u) ↦ X)
              ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map
                  (Quiver.Hom.op
                    (IsTerminal.from
                      (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))
                      (fiber (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f
                        x)))) :
              (a :
                  X.obj
                    (Opposite.op
                      (CompHausLike.of
                        (fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
                        PUnit.{u + 1}))) →
                X.obj (Opposite.op (fiber f x)))
            (Function.Fiber.image
              (⇑f :
                (a : (Opposite.unop Y).obj) →
                  X.obj
                    (Opposite.op
                      (CompHausLike.of
                        (fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
                        PUnit.{u + 1})))
              x) :
          X.obj
            (Opposite.op
              (fiber (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x))) :
      (fun (X : Type u) ↦ X)
        ((↑((fiber (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u) →
          X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))

Tactic:
ext y