-- Mathlib/Topology/UniformSpace/Compact.lean
theorem IsCompact.nhdsSet_basis_uniformity {p : ι → Prop} {V : ι → Set (α × α)}
    (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) :
    (𝓝ˢ K).HasBasis p fun i => ⋃ x ∈ K, ball x (V i) where
  mem_iff' U

Proof state:
case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Tactic:
rintro ⟨i, hpi, hi⟩

Result:
case mpr.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K

Proof state:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
intro H

Result:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Proof state:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
have HKU : K ⊆ ⋃ _ : Unit, interior U := by
  simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H

Result:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
constructor

Result:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Proof state:
case mpr.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K

Tactic:
refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi

Result:
case mpr.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
x✝ : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x

Proof state:
case mpr.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
x✝ : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x

Tactic:
exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi

Result:
no goals

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ K ⊆ ⋃ x, interior U

Tactic:
simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H

Result:
no goals

Proof state:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
  simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

Result:
case mp.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Proof state:
case mp.intro.intro
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
exact ⟨i, hpi, hi.trans interior_subset⟩

Result:
no goals

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U

Tactic:
simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

Result:
no goals