-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
    [TopologicalSpace β] {k s : Set β} {f : β → α} (hk : IsCompact k)
    (hf : ∀ x ∈ k, ContinuousWithinAt f s x) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this
  with ⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
have : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α)) := by
  rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
  exact fun x hx ↦ disjoint_left_comm.2 <|
    tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)

Tactic:
exact fun x hx ↦ disjoint_left_comm.2 <|
  tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ f '' (U ∩ s) ⊆ tᶜ

Tactic:
rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ f '' (U ∩ s) ⊆ tᶜ

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))

Tactic:
rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)