-- Module: Mathlib.Topology.Category.LightProfinite.Basic
Goal:
S : LightDiagram
a :
  LocallyConstant (↑(S.cone.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
    (Fin 2)
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
⊢ ∃ (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

Premises used: LightDiagram.cone, Profinite.exists_locallyConstant, LightDiagram.isLimit