-- Mathlib/MeasureTheory/Measure/DiracProba.lean
lemma CompletelyRegularSpace.exists_BCNN {X : Type*} [TopologicalSpace X] [CompletelyRegularSpace X]
    {K : Set X} (K_closed : IsClosed K) {x : X} (x_notin_K : x ∉ K) :
    ∃ (f : X →ᵇ ℝ≥0), f x = 1 ∧ (∀ y ∈ K, f y = 0)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
y : X
y_in_K : y ∈ K
⊢ f y = 0

Tactic:
simp [f, g', g_one_on_K y_in_K, tsub_self]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ f x = 1

Tactic:
simp [f, g', gx_zero]

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
refine ⟨f, by simp [f, g', gx_zero], fun y y_in_K ↦ by simp [f, g', g_one_on_K y_in_K, tsub_self]⟩

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
set f := 1 - g'

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x✝ : X
x_notin_K : x✝ ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x✝ = 0
g_one_on_K : EqOn g 1 K
x y : X
⊢ ↑1 * dist ↑(g x) ↑(g y) ≤ 1

Tactic:
simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
obtain ⟨g, g_cont, gx_zero, g_one_on_K⟩ :=
  CompletelyRegularSpace.completely_regular x K K_closed x_notin_K

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
have g_bdd : ∀ x y, dist (Real.toNNReal (g x)) (Real.toNNReal (g y)) ≤ 1 := by
  refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_
  simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
set g' := BoundedContinuousFunction.mkOfBound
    ⟨fun x ↦ Real.toNNReal (g x), continuous_real_toNNReal.comp g_cont.subtype_val⟩ 1 g_bdd

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1

Tactic:
refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed K
x✝ : X
x_notin_K : x✝ ∉ K
g : X → ↑unitInterval
g_cont : Continuous g
gx_zero : g x✝ = 0
g_one_on_K : EqOn g 1 K
x y : X
⊢ ↑1 * dist ↑(g x) ↑(g y) ≤ 1