-- Module: Mathlib.Topology.Category.LightProfinite.AsLimit
Goal:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
hc : IsLimit c := S.toLightDiagram.isLimit
⊢ Eq (α :=
    lightToProfinite.obj S ⟶
      lightToProfinite.obj (FintypeCat.toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))))
    (ConcreteCategory.ofHom (FC :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
          (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
        (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (TopCat.Hom.hom (S.proj n).hom) :
      Quiver.Hom (V := CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
        (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
          (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
          (↑((FintypeCat.toLightProfinite.obj (S.fintypeDiagram.obj (Opposite.op n))).toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)))
    (NatTrans.app (Cone.π (lightToProfinite.obj S).asLimitCone)
        (Functor.obj
          (IsCofiltered.sequentialFunctor
            (DiscreteQuotient
              (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)))
          (Opposite.op n)) :
      Functor.obj (C :=
          DiscreteQuotient
            (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u))
          (Functor.obj
            (Functor.const
              (DiscreteQuotient
                (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)))
            (Cone.pt (J :=
              DiscreteQuotient
                (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u))
              (lightToProfinite.obj S).asLimitCone))
          (Functor.obj
            (IsCofiltered.sequentialFunctor
              (DiscreteQuotient
                (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)))
            (Opposite.op n)) ⟶
        Functor.obj (C :=
          DiscreteQuotient
            (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u))
          (lightToProfinite.obj S).diagram
          (Functor.obj
            (IsCofiltered.sequentialFunctor
              (DiscreteQuotient
                (↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)))
            (Opposite.op n)))

Tactic:
exact liftedLimitMapsToOriginal_inv_map_π hc _

Premises used: CategoryTheory.liftedLimitMapsToOriginal_inv_map_π