-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (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))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
H₁ :
  ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ≤ Q₂ →
      Superset (α := Set (↑C : Type u))
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₁)})
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₂)})
obtain :
  ∀ (x : (↑C : Type u))
    (hx :
      Membership.mem (γ := Set (↑C : Type u))
        (⋂ (J : Finset ι),
          Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
            (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
            {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
                (op J)})
        x),
    ∃ (x : (↑C : Type u)),
      ∀ (J : Finset ι),
        (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
          (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op J)
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)

Tactic:
obtain ⟨x, hx⟩ :
            Set.Nonempty (⋂ (J : Finset ι), π_app C (· ∈ J) ⁻¹' {a.val (op J)}) :=
          IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
            (fun J : Finset ι => π_app C (· ∈ J) ⁻¹' {a.val (op J)}) (directed_of_isDirected_le H₁)
            (fun J => (Set.singleton_nonempty _).preimage (surjective_π_app _))
            (fun J => (hc J (a.val (op J))).isCompact) fun J => hc J (a.val (op J))

Premises used: Set.singleton_nonempty, Set.iInter, Membership.mem, Profinite.IndexFunctor.surjective_π_app, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, directed_of_isDirected_le, Set.Nonempty, Set.preimage, Opposite.op, IsClosed.isCompact, Set.Nonempty.preimage, Singleton.singleton, Subtype.val, DFunLike.coe, Profinite.IndexFunctor.π_app