-- Module: Mathlib.Topology.Category.LightProfinite.AsLimit
Goal:
S : LightProfinite
n : ℕ
rw :
  Function.Surjective (α :=
    (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))
      (lightToProfinite.obj S))
    (β :=
    (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))
      (lightToProfinite.obj (S.diagram.obj (Opposite.op n))))
    (⇑(ConcreteCategory.hom (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)) (X :=
            lightToProfinite.obj S) (Y := lightToProfinite.obj (S.diagram.obj (Opposite.op n)))
            (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))) :
          C((↑((lightToProfinite.obj S).toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u),
            (↑((lightToProfinite.obj (S.diagram.obj (Opposite.op n))).toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
              Type u))) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            (lightToProfinite.obj S)) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
          (lightToProfinite.obj (S.diagram.obj (Opposite.op n))))
⊢ Function.Surjective (α :=
    (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))
      (lightToProfinite.obj S))
    (β :=
    (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))
      (lightToProfinite.obj (S.diagram.obj (Opposite.op n))))
    (⇑(ConcreteCategory.hom (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))
          (lightToProfinite.map (S.proj n))) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            (lightToProfinite.obj S)) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
          (lightToProfinite.obj (S.diagram.obj (Opposite.op n))))

Tactic:
rw [lightToProfinite_map_proj_eq]

Premises used: LightProfinite.lightToProfinite_map_proj_eq