-- 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)
refine_1 :
  ∀
    (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)),
    a = b
refine_2 :
  ∀
    (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),
    ∃ (a_1 :
      (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))),
      (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_1 =
        a
⊢ Function.Bijective (α :=
    (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)))
    (β :=
    (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)

Tactic:
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩