-- Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
theorem exists_continuous_nnreal_forall_closedBall_subset (hK : ∀ i, IsClosed (K i))
    (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
    ∃ δ : C(X, ℝ≥0), (∀ x, 0 < δ x) ∧ ∀ (i), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
rcases exists_continuous_real_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < (ContinuousMap.coeNNRealReal.comp δ) x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ) x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
refine ⟨δ, hδ₀, fun i x hi => ?_⟩

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < (ContinuousMap.coeNNRealReal.comp δ) x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ) x)) ⊆ U i
i : ι
x : X
hi : x ∈ K i
⊢ closedBall x ↑(δ x) ⊆ U i

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < (ContinuousMap.coeNNRealReal.comp δ) x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ) x)) ⊆ U i
i : ι
x : X
hi : x ∈ K i
⊢ closedBall x ↑(δ x) ⊆ U i

Tactic:
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), 0 < δ x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Tactic:
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < (ContinuousMap.coeNNRealReal.comp δ) x
hδ : ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ) x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i