-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.AsLimit (goal)
Goal:
S : LightProfinite
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))))
have 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))))
Tactic: rw [lightToProfinite_map_proj_eq]