awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
h :
  ∀ (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))
i : ι
⊢ Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        a :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        b :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))

Tactic:
specialize h ({i} : Finset ι)

Premises used: Singleton.singleton
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
i : ι
h :
  Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        a :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        b :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
⊢ Eq.{u + 1} (α := (i_1 : ↥{i}) → X (↑i_1 : ι))
    (↑((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
            (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
          a) :
      (i_1 : ↥{i}) → X (↑i_1 : ι))
    (↑((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
            (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
          b) :
      (i_1 : ↥{i}) → X (↑i_1 : ι))

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
i : ι
h :
  Eq.{u + 1} (α := (i_1 : ↥{i}) → X (↑i_1 : ι)) (fun (j : ↥{i}) ↦ (↑a : (i : ι) → X i) (↑j : ι)) fun (j : ↥{i}) ↦
    (↑b : (i : ι) → X i) (↑j : ι)
⊢ (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i

Tactic:
congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

Premises used: Iff.mpr, Finset.mem_singleton, Subtype.mk, congr_fun, rfl
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
i : ι
h :
  Eq.{u + 1} (α := (i_1 : ↥{i}) → X (↑i_1 : ι)) (fun (j : ↥{i}) ↦ (↑a : (i : ι) → X i) (↑j : ι)) fun (j : ↥{i}) ↦
    (↑b : (i : ι) → X i) (↑j : ι)
⊢ (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i

Tactic:
exact congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

Premises used: Iff.mpr, Finset.mem_singleton, Subtype.mk, congr_fun, rfl
-- Module: Mathlib.Topology.Category.Profinite.Product
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
J : (Finset ι)ᵒᵖ
rw : IsCompact (X := (i : ↥(unop J)) → X (↑i : ι)) (obj (X := X) C fun (x : ι) ↦ x ∈ unop J)
⊢ CompactSpace.{u} (↑(obj (X := X) C fun (x : ι) ↦ x ∈ unop J) : Type u)

Tactic:
rw [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.Category.Profinite.Product
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
J : (Finset ι)ᵒᵖ
⊢ IsCompact (X := (i : ↥(unop J)) → X (↑i : ι)) (obj (X := X) C fun (x : ι) ↦ x ∈ unop J)

Tactic:
hC.image (Pi.continuous_precomp' _)

Premises used: Pi.continuous_precomp', IsCompact.image, Profinite.IndexFunctor.obj
-- Module: Mathlib.Topology.Category.Profinite.Product
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
J : (Finset ι)ᵒᵖ
⊢ IsCompact (X := (i : ↥(unop J)) → X (↑i : ι)) (obj (X := X) C fun (x : ι) ↦ x ∈ unop J)

Tactic:
exact hC.image (Pi.continuous_precomp' _)

Premises used: Pi.continuous_precomp', IsCompact.image
-- 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 rwa rwa₁ rwa₂ rwa₃ : IsCompact C
⊢ CompactSpace.{u} (↑C : Type u)

Tactic:
rwa [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- 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)
⊢ 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:
⟨fun a b h ↦ ?_, fun a ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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
b : (↑C : Type u)
hb :
  ∀ (J : Finset ι),
    (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) b =
      (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
J : (Finset ι)ᵒᵖ
⊢ (↑((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))
      J =
    (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) J

Tactic:
hb (unop J)

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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
b : (↑C : Type u)
hb :
  ∀ (J : Finset ι),
    (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) b =
      (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
J : (Finset ι)ᵒᵖ
⊢ (↑((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))
      J =
    (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) J

Tactic:
exact hb (unop J)

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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 ι
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})

Tactic:
IsClosed.preimage (π_app C (· ∈ J)).continuous ?_

Premises used: ContinuousMap.continuous, Membership.mem, IsClosed.preimage, Profinite.IndexFunctor.π_app
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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 ι
s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)
refine : IsClosed (X := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) {s}
⊢ 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})

Tactic:
refine IsClosed.preimage (π_app C (· ∈ J)).continuous ?_

Premises used: ContinuousMap.continuous, Membership.mem, IsClosed.preimage, Profinite.IndexFunctor.π_app
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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 ι
s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)
⊢ IsClosed (X := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) {s}

Tactic:
T1Space.t1 s

Premises used: T1Space.t1
-- Module: Mathlib.Topology.Category.Profinite.Product
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 :
  (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 ι
s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)
⊢ IsClosed (X := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) {s}

Tactic:
exact T1Space.t1 s

Premises used: T1Space.t1
-- 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
⊢ ∀ (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})

Tactic:
have hc : ∀ (J : Finset ι) s, IsClosed ((π_app C (· ∈ J)) ⁻¹' {s}) := by
          intro J s
          refine IsClosed.preimage (π_app C (· ∈ J)).continuous ?_
          exact T1Space.t1 s
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K_1 : ι → 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})
J K : Finset ι
h : J ≤ K
x : (↑C : Type u)
hx :
  Membership.mem (γ := Set (↑C : Type u))
    (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
      (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ K) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u))
      {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
          (op K)})
    x
⊢ Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
    {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op K)}
    ((π_app (X := X) C fun (x : ι) ↦ x ∈ K : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u)) x :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))

Tactic:
simp only [Set.mem_preimage] at hx ⊢

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K_1 : ι → 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})
J K : Finset ι
h : J ≤ K
x : (↑C : Type u)
hx :
  Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
    {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op K)}
    ((π_app (X := X) C fun (x : ι) ↦ x ∈ K : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u)) x :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
⊢ Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
    (singleton (α :=
      (↑(((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op) :
            (a : (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op K)) : Type u)) →
              (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u))
          ((↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op K)) :
        (↑(((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u)))
    ((map (X := X) C (J := Membership.mem J) (K := Membership.mem K) h :
          (a : (↑(obj C (Membership.mem K)) : Type u)) → (↑(obj C (Membership.mem J)) : Type u))
        ((↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
          (op K)) :
      (↑(obj (X := X) C (Membership.mem J)) : Type u))

Tactic:
rfl
-- 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})
⊢ ∀ (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₂)})

Tactic:
have H₁ : ∀ (Q₁ Q₂ : Finset ι), Q₁ ≤ Q₂ →
            π_app C (· ∈ Q₁) ⁻¹' {a.val (op Q₁)} ⊇
            π_app C (· ∈ Q₂) ⁻¹' {a.val (op Q₂)} := by
          intro J K h x hx
          simp only [Set.mem_preimage] at hx ⊢
          rw [← map_comp_π_app C h, Function.comp_apply,
            hx, ← a.prop (homOfLE h).op]
          rfl