-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.disjoint_nhdsSet_left {l : Filter X} (hs : IsCompact s) :
    Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ∀ i ∈ t, (U i)ᶜ ∈ l

Tactic:
exact fun x hx => hUl x (hts x hx)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ (⋃ x ∈ t, U x)ᶜ ∈ l

Tactic:
rw [compl_iUnion₂, biInter_finset_mem]

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ∀ i ∈ t, (U i)ᶜ ∈ l

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x ∧ IsOpen (U x)
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ Disjoint (𝓝ˢ s) l

Tactic:
refine (hasBasis_nhdsSet _).disjoint_iff_left.2
  ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ (⋃ x ∈ t, U x)ᶜ ∈ l

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
⊢ Disjoint (𝓝ˢ s) l

Tactic:
rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ Disjoint (𝓝ˢ s) l

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x ∧ IsOpen (U x)
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
choose hxU hUo using hxU

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen (U x)
⊢ Disjoint (𝓝ˢ s) l