-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
have have₁ have₂ :
  ∀ (this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₃ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₄ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i),
      ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₅ have₆ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₇ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      let U := Sᶜ.pi (α := R) K;
      ∀ (U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
have₈ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      let U := Sᶜ.pi (α := R) K;
      ∀ (U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a))
        (QU :
          Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)),
        ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
refine_1 :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      let U := Sᶜ.pi (α := R) K;
      ∀ (U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a))
        (QU :
          Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)),
        IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)
refine_2 refine_2₁ :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)),
    let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
    ∀ (Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i) (Q_compact : IsCompact Q),
      let U := Sᶜ.pi (α := R) K;
      ∀ (U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a))
        (QU :
          Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)),
        DFunLike.coe (β := R) ⁻¹' U ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds

Premises used: Topology.IsInducing.nhds_eq_comap, RestrictedProduct.isEmbedding_coe_of_principal, Set.inter_subset_left, RestrictedProduct.range_coe_principal, Set.pi_if, Set.mem_univ, Topology.IsEmbedding.toIsInducing, true_and, Set