-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Basic (goal)
Goal:
S : LightDiagram
a :
  LocallyConstant (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
    (Fin 2)
⊢ ∃ (a_1 :
    (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2)),
    (fun
            (a :
              (n : ℕ) ×
                LocallyConstant
                  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)
                  (Fin 2)) ↦
          LocallyConstant.comap
            (TopCat.Hom.hom
              (InducedCategory.Hom.hom
                (S.cone.π.app
                  (op
                    (a.fst (β := fun (n : ℕ) ↦
                      LocallyConstant
                        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)
                        (Fin 2)))))))
            (a.snd (β := fun (n : ℕ) ↦
              LocallyConstant
                (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)
                (Fin 2))))
        a_1 =
      a
have refine_3 : ∀ (n : ℕᵒᵖ)
  (g :
    LocallyConstant
      (↑(((S.diagram ⋙ toProfinite).obj n).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      (Fin 2))
  (h : a = LocallyConstant.comap (TopCat.Hom.hom (S.cone.π.app n).hom) g),
  ∃ (a_1 :
    (n : ℕ) ×
      LocallyConstant
        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u)
        (Fin 2)),
    (fun
            (a :
              (n : ℕ) ×
                LocallyConstant
                  (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                    Type u)
                  (Fin 2)) ↦
          LocallyConstant.comap
            (TopCat.Hom.hom
              (InducedCategory.Hom.hom
                (S.cone.π.app
                  (op
                    (a.fst (β := fun (n : ℕ) ↦
                      LocallyConstant
                        (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)
                        (Fin 2)))))))
            (a.snd (β := fun (n : ℕ) ↦
              LocallyConstant
                (↑(((S.diagram ⋙ toProfinite).obj (op n)).toTop (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                  Type u)
                (Fin 2))))
        a_1 =
      a
Tactic: obtain ⟨n, g, h⟩ := Profinite.exists_locallyConstant S.cone S.isLimit a