X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
⊢ ⊤ ≤ closure L
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
⊢ closure L = ⊤
apply eq_top_iff.mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
⊢ f ∈ closure L
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
⊢ ⊤ ≤ closure L
rintro f -
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x, x ∈ Metric.ball f ε ∧ x ∈ L
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
⊢ f ∈ closure L
refine'
  Filter.Frequently.mem_closure
    ((Filter.HasBasis.frequently_iff Metric.nhds_basis_ball).mpr fun ε pos => _)
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x, dist x f < ε ∧ x ∈ L
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x, x ∈ Metric.ball f ε ∧ x ∈ L
simp only [exists_prop, Metric.mem_ball]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : ¬Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x, dist x f < ε ∧ x ∈ L
by_cases nX : Nonempty X
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : ¬Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : ¬Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
swap
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : ¬Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L

case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
exact ⟨nA.some, (dist_lt_iff pos).mpr fun x => False.elim (nX ⟨x⟩), nA.choose_spec⟩
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : Set.SeparatesPointsStrongly L
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
dsimp only [Set.SeparatesPointsStrongly] at sep
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ x, dist x f < ε ∧ x ∈ L
choose g hg w₁ w₂ using sep f
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let U : X → X → Set X := fun x y => {z | f z - ε < g x y z}
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let ys : ∀ _, Finset X := fun x => (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x)).choose
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let ys_w : ∀ x, (⋃ y ∈ ys x, U x y) = ⊤ := fun x =>
  (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x)).choose_spec
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
⊢ ∃ x, dist x f < ε ∧ x ∈ L
have ys_nonempty : ∀ x, (ys x).Nonempty := fun x =>
  Set.nonempty_of_union_eq_top_of_nonempty _ _ nX (ys_w x)
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let h : ∀ _, L := fun x =>
  ⟨(ys x).sup' (ys_nonempty x) fun y => (g x y : C(X, ℝ)),
    Finset.sup'_mem _ sup_mem _ _ _ fun y _ => hg x y⟩
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
⊢ ∃ x, dist x f < ε ∧ x ∈ L
have lt_h : ∀ x z, f z - ε < (h x : X → ℝ) z := by
  intro x z
  obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
  dsimp
  simp only [Subtype.coe_mk, sup'_coe, Finset.sup'_apply, Finset.lt_sup'_iff]
  exact ⟨y, ym, zm⟩
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
⊢ ∃ x, dist x f < ε ∧ x ∈ L
have h_eq : ∀ x, (h x : X → ℝ) x = f x := by intro x; simp [w₁]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let W : ∀ _, Set X := fun x => {z | (h x : X → ℝ) z < f z + ε}
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let xs : Finset X := (CompactSpace.elim_nhds_subcover W W_nhd).choose
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let xs_w : (⋃ x ∈ xs, W x) = ⊤ := (CompactSpace.elim_nhds_subcover W W_nhd).choose_spec
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
⊢ ∃ x, dist x f < ε ∧ x ∈ L
have xs_nonempty : xs.Nonempty := Set.nonempty_of_union_eq_top_of_nonempty _ _ nX xs_w
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ ∃ x, dist x f < ε ∧ x ∈ L
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
⊢ ∃ x, dist x f < ε ∧ x ∈ L
let k : (L : Type _) :=
  ⟨xs.inf' xs_nonempty fun x => (h x : C(X, ℝ)),
    Finset.inf'_mem _ inf_mem _ _ _ fun x _ => (h x).2⟩
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ dist (↑k) f < ε
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ ∃ x, dist x f < ε ∧ x ∈ L
refine' ⟨k.1, _, k.2⟩
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ ∀ (x : X), dist (↑↑k x) (↑f x) < ε
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ dist (↑k) f < ε
rw [dist_lt_iff pos]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ dist (↑↑k z) (↑f z) < ε
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
⊢ ∀ (x : X), dist (↑↑k x) (↑f x) < ε
intro z
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑↑k z < ↑f z + ε ∧ ↑f z - ε < ↑↑k z
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ dist (↑↑k z) (↑f z) < ε
rw [show ∀ a b ε : ℝ, dist a b < ε ↔ a < b + ε ∧ b - ε < a by
      intros; simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]]
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑↑k z < ↑f z + ε

case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑f z - ε < ↑↑k z
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑↑k z < ↑f z + ε ∧ ↑f z - ε < ↑↑k z
fconstructor
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ U x y ∈ 𝓝 y
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
⊢ ∀ (x y : X), U x y ∈ 𝓝 y
intro x y
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ IsOpen (U x y)

case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ y ∈ U x y
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ U x y ∈ 𝓝 y
refine' IsOpen.mem_nhds _ _
no goals
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ IsOpen (U x y)
apply isOpen_lt <;> continuity
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ ↑f y - ε < ↑f y
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ y ∈ U x y
rw [Set.mem_setOf_eq, w₂]
no goals
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
x y : X
⊢ ↑f y - ε < ↑f y
exact sub_lt_self _ pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z : X
⊢ ↑f z - ε < ↑↑(h x) z
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
⊢ ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
intro x z
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ↑f z - ε < ↑↑(h x) z
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z : X
⊢ ↑f z - ε < ↑↑(h x) z
obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ↑f z - ε <
    ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ↑f z - ε < ↑↑(h x) z
dsimp
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ∃ b,
    b ∈ Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤) ∧ ↑f z - ε < ↑(g x b) z
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ↑f z - ε <
    ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
simp only [Subtype.coe_mk, sup'_coe, Finset.sup'_apply, Finset.lt_sup'_iff]
no goals
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
x z y : X
ym : y ∈ fun i => i ∈ (ys x).val
zm : z ∈ U x y
⊢ ∃ b,
    b ∈ Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤) ∧ ↑f z - ε < ↑(g x b) z
exact ⟨y, ym, zm⟩
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
x : X
⊢ ↑↑(h x) x = ↑f x
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
⊢ ∀ (x : X), ↑↑(h x) x = ↑f x
intro x
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
x : X
⊢ ↑↑(h x) x = ↑f x
simp [w₁]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ W x ∈ 𝓝 x
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
⊢ ∀ (x : X), W x ∈ 𝓝 x
intro x
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ IsOpen (W x)

case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ x ∈ W x
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ W x ∈ 𝓝 x
refine' IsOpen.mem_nhds _ _
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ Continuous fun b => ↑f b + ε
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ IsOpen (W x)
apply isOpen_lt (continuous_set_coe _ _)
no goals
case refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ Continuous fun b => ↑f b + ε
continuity
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      x <
    ↑f x + ε
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ x ∈ W x
dsimp only [Set.mem_setOf_eq]
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ ↑f x < ↑f x + ε
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      x <
    ↑f x + ε
rw [h_eq]
no goals
case refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
x : X
⊢ ↑f x < ↑f x + ε
exact lt_add_of_pos_right _ pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
a✝ b✝ ε✝ : ℝ
⊢ dist a✝ b✝ < ε✝ ↔ a✝ < b✝ + ε✝ ∧ b✝ - ε✝ < a✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ∀ (a b ε : ℝ), dist a b < ε ↔ a < b + ε ∧ b - ε < a
intros
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
a✝ b✝ ε✝ : ℝ
⊢ dist a✝ b✝ < ε✝ ↔ a✝ < b✝ + ε✝ ∧ b✝ - ε✝ < a✝
simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑(Finset.inf'
          (Exists.choose
            (_ :
              ∃ t,
                (⋃ (x : X) (_ : x ∈ t),
                    {z |
                      ↑(Finset.sup'
                              (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                              (_ : Finset.Nonempty (ys x)) fun y => g x y)
                          z <
                        ↑f z + ε}) =
                  ⊤))
          xs_nonempty fun x =>
          Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
            (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z <
    ↑f z + ε
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑↑k z < ↑f z + ε
dsimp
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ∃ i,
    i ∈
        Exists.choose
          (_ :
            ∃ t,
              (⋃ (x : X) (_ : x ∈ t),
                  {z |
                    ↑(Finset.sup'
                            (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                            (_ : Finset.Nonempty (ys x)) fun y => g x y)
                        z <
                      ↑f z + ε}) =
                ⊤) ∧
      ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), {z | ↑f z - ε < ↑(g i x) z}) = ⊤))
              (_ : Finset.Nonempty (ys i)) fun y => g i y)
          z <
        ↑f z + ε
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑(Finset.inf'
          (Exists.choose
            (_ :
              ∃ t,
                (⋃ (x : X) (_ : x ∈ t),
                    {z |
                      ↑(Finset.sup'
                              (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                              (_ : Finset.Nonempty (ys x)) fun y => g x y)
                          z <
                        ↑f z + ε}) =
                  ⊤))
          xs_nonempty fun x =>
          Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
            (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z <
    ↑f z + ε
simp only [Finset.inf'_lt_iff, ContinuousMap.inf'_apply]
no goals
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ∃ i,
    i ∈
        Exists.choose
          (_ :
            ∃ t,
              (⋃ (x : X) (_ : x ∈ t),
                  {z |
                    ↑(Finset.sup'
                            (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                            (_ : Finset.Nonempty (ys x)) fun y => g x y)
                        z <
                      ↑f z + ε}) =
                ⊤) ∧
      ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), {z | ↑f z - ε < ↑(g i x) z}) = ⊤))
              (_ : Finset.Nonempty (ys i)) fun y => g i y)
          z <
        ↑f z + ε
exact Set.exists_set_mem_of_union_eq_top _ _ xs_w z
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑f z - ε <
    ↑(Finset.inf'
          (Exists.choose
            (_ :
              ∃ t,
                (⋃ (x : X) (_ : x ∈ t),
                    {z |
                      ↑(Finset.sup'
                              (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                              (_ : Finset.Nonempty (ys x)) fun y => g x y)
                          z <
                        ↑f z + ε}) =
                  ⊤))
          xs_nonempty fun x =>
          Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
            (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑f z - ε < ↑↑k z
dsimp
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ∀ (i : X),
    i ∈
        Exists.choose
          (_ :
            ∃ t,
              (⋃ (x : X) (_ : x ∈ t),
                  {z |
                    ↑(Finset.sup'
                            (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                            (_ : Finset.Nonempty (ys x)) fun y => g x y)
                        z <
                      ↑f z + ε}) =
                ⊤) →
      ↑f z - ε <
        ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), {z | ↑f z - ε < ↑(g i x) z}) = ⊤))
              (_ : Finset.Nonempty (ys i)) fun y => g i y)
          z
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ↑f z - ε <
    ↑(Finset.inf'
          (Exists.choose
            (_ :
              ∃ t,
                (⋃ (x : X) (_ : x ∈ t),
                    {z |
                      ↑(Finset.sup'
                              (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                              (_ : Finset.Nonempty (ys x)) fun y => g x y)
                          z <
                        ↑f z + ε}) =
                  ⊤))
          xs_nonempty fun x =>
          Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
            (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
simp only [Finset.lt_inf'_iff, ContinuousMap.inf'_apply]
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z x : X
⊢ ↑f z - ε <
    ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z : X
⊢ ∀ (i : X),
    i ∈
        Exists.choose
          (_ :
            ∃ t,
              (⋃ (x : X) (_ : x ∈ t),
                  {z |
                    ↑(Finset.sup'
                            (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
                            (_ : Finset.Nonempty (ys x)) fun y => g x y)
                        z <
                      ↑f z + ε}) =
                ⊤) →
      ↑f z - ε <
        ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), {z | ↑f z - ε < ↑(g i x) z}) = ⊤))
              (_ : Finset.Nonempty (ys i)) fun y => g i y)
          z
rintro x -
no goals
case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : Set.Nonempty L
inf_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊓ g ∈ L
sup_mem : ∀ (f : C(X, ℝ)), f ∈ L → ∀ (g : C(X, ℝ)), g ∈ L → f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f, f ∈ L ∧ ↑f x = v x ∧ ↑f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), ↑(g x y) x = ↑f x
w₂ : ∀ (x y : X), ↑(g x y) y = ↑f y
U : X → X → Set X := fun x y => {z | ↑f z - ε < ↑(g x y) z}
U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x => Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), U x x_1) = ⊤)
ys_w : ∀ (x : X), (⋃ (y : X) (_ : y ∈ ys x), U x y) = ⊤ :=
  fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))
ys_nonempty : ∀ (x : X), Finset.Nonempty (ys x)
h : X → ↑L :=
  fun x =>
    { val := Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y,
      property := (_ : (Finset.sup' (ys x) (_ : Finset.Nonempty (ys x)) fun y => g x y) ∈ L) }
lt_h : ∀ (x z : X), ↑f z - ε < ↑↑(h x) z
h_eq : ∀ (x : X), ↑↑(h x) x = ↑f x
W : X → Set X := fun x => {z | ↑↑(h x) z < ↑f z + ε}
W_nhd : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := Exists.choose (_ : ∃ t, (⋃ (x : X) (_ : x ∈ t), W x) = ⊤)
xs_w : (⋃ (x : X) (_ : x ∈ xs), W x) = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhd)
xs_nonempty : Finset.Nonempty xs
k : ↑L :=
  { val := Finset.inf' xs xs_nonempty fun x => ↑(h x),
    property := (_ : (Finset.inf' xs xs_nonempty fun x => ↑(h x)) ∈ L) }
z x : X
⊢ ↑f z - ε <
    ↑(Finset.sup' (Exists.choose (_ : ∃ t, (⋃ (x_1 : X) (_ : x_1 ∈ t), {z | ↑f z - ε < ↑(g x x_1) z}) = ⊤))
          (_ : Finset.Nonempty (ys x)) fun y => g x y)
      z
apply lt_h