-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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})))
⊢ 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 x))))
    ((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 : (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 x))))
        (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 x))))
    ((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 : (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 x))))
        (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 x))))
have w : Eq (α :=
  X.obj
    (Opposite.op
      (fiber (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x)))
  ((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)))
  ((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 (FC := TypeCat.Fun)
              (counitAppApp (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (LightProfinite.of (Opposite.unop Y).obj) X) :
            (a :
                LocallyConstant (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.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj)))
          f :
        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)))
Tactic: dsimp [toLightProfinite_obj]