-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a b :
  (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))
    (Cone.pt (F := indexFunctor (X := X) (C := C) hC) (indexCone (X := X) (C := C) hC))
h :
  Eq (α :=
    (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)
    ((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 :=
            Cone.pt (F := indexFunctor (X := X) (C := C) hC) (indexCone (X := X) (C := C) hC))
            ((limitConeIsLimit (indexFunctor (X := X) (C := C) hC)).lift (indexCone (X := X) (C := C) hC)) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (indexCone hC).pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone (indexFunctor hC)).pt)
        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)
    ((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 :=
            Cone.pt (F := indexFunctor (X := X) (C := C) hC) (indexCone (X := X) (C := C) hC))
            ((limitConeIsLimit (indexFunctor (X := X) (C := C) hC)).lift (indexCone (X := X) (C := C) hC)) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (indexCone hC).pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone (indexFunctor hC)).pt)
        b :
      (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)
J : Finset ι
⊢ Eq (α := (↑(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 :
      (↑(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)) b :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
have h₁ : Eq.{u + 1} (α := (↑(((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u))
  ((↑((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 :=
              Cone.pt (F := indexFunctor (X := X) (C := C) hC) (indexCone (X := X) (C := C) hC))
              ((limitConeIsLimit (indexFunctor (X := X) (C := C) hC)).lift (indexCone (X := X) (C := C) hC)) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (indexCone hC).pt) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (limitCone (indexFunctor hC)).pt)
          a) :
      (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
    (op J))
  ((↑((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 :=
              Cone.pt (F := indexFunctor (X := X) (C := C) hC) (indexCone (X := X) (C := C) hC))
              ((limitConeIsLimit (indexFunctor (X := X) (C := C) hC)).lift (indexCone (X := X) (C := C) hC)) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (indexCone hC).pt) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (limitCone (indexFunctor hC)).pt)
          b) :
      (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
    (op J))
Tactic: apply_fun fun f : (limitCone.{u, u} (indexFunctor hC)).pt => f.val (op J) at h
Cleared hypotheses: h