-- 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))
rw :
  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))
⊢ Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
    {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)}
    ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))

Tactic:
rw [← map_comp_π_app C h, Function.comp_apply,
            hx, ← a.prop (homOfLE h).op]

Premises used: Quiver.Hom.op, Profinite.IndexFunctor.map_comp_π_app, CategoryTheory.homOfLE, Subtype.prop, Function.comp_apply