-- 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)
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)
            (X.map
              (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (LightProfinite.of PUnit.{u + 1}) y ≫
                  sigmaIncl (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).op) :
          (a : X.obj (Opposite.op (LightProfinite.of (Opposite.unop Y).obj))) →
            X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
        (((@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 (LightProfinite.of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 (LightProfinite.of PUnit.{u + 1})))) :
          (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 (LightProfinite.of PUnit.{u + 1})))
        (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 (LightProfinite.of PUnit.{u + 1})))

Tactic:
simpa [← dsimp% isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u} f x),
    ← isoFinYonedaComponents_hom_apply, -isoFinYonedaComponents_hom] using x.map_eq_image f y

Premises used: LightCondensed.isoFinYonedaComponents_hom_apply, LightCondensed.isoFinYonedaComponents_hom, Function.Fiber.map_eq_image, DFunLike.coe