-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.mem_nhdsSet_prod_of_forall {K : Set X} {Y} {l : Filter Y} {s : Set (X × Y)}
    (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l) : s ∈ (𝓝ˢ K) ×ˢ l

Proof state:
case refine_3.intro.mk.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen (u, v).1
⊢ (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l

Tactic:
exact prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv

Result:
no goals

Proof state:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

Tactic:
simp [sup_prod, *]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ ∅ ×ˢ l

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l

Tactic:
refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_

Result:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

case refine_2
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Proof state:
case refine_3.intro.mk.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩

Result:
case refine_3.intro.mk.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen (u, v).1
⊢ (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l

Proof state:
case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
  with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩

Result:
case refine_3.intro.mk.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Proof state:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

Tactic:
exact prod_mono (nhdsSet_mono ht) le_rfl hs

Result:
no goals