-- Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
theorem eventually_nhds_zero_forall_closedBall_subset (hK : ∀ i, IsClosed (K i))
    (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) (x : X) :
    ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, ∀ i, p.2 ∈ K i → closedBall p.2 p.1 ⊆ 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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.2 p.1
⊢ p.1 < ↑r

Tactic:
exact hp.1

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
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.mp hR₀ with ⟨r, hr₀, hrR⟩

Result:
case intro.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
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i

Proof state:
case h.mk
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
r : ℝ≥0∞
y : X
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ i ∈ {b | x ∈ K b}, closedBall x_2.2 x_2.1 ⊆ U i) x_1}
i : ι
hi : (r, y).2 ∈ K i
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedBall (r, y).2 (r, y).1 ⊆ U i

Tactic:
exact hyU _ (hxy _ hi)

Result:
no goals

Proof state:
case h
ι : 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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.2 p.1
⊢ z ∈ U i

Tactic:
apply hR

Result:
case h.a
ι : 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
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.2 p.1
⊢ z ∈ closedBall x R

Proof state:
case h.mk
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
r : ℝ≥0∞
y : X
hxy : (r, y) ∈ Prod.snd ⁻¹' ⋂ i, ⋂ (_ : x ∉ K i), (K i)ᶜ
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ i ∈ {b | x ∈ K b}, closedBall x_2.2 x_2.1 ⊆ U i) x_1}
i : ι
hi : (r, y).2 ∈ K i
⊢ closedBall (r, y).2 (r, y).1 ⊆ U i

Tactic:
simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy

Result:
case h.mk
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
r : ℝ≥0∞
y : X
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ i ∈ {b | x ∈ K b}, closedBall x_2.2 x_2.1 ⊆ U i) x_1}
i : ι
hi : (r, y).2 ∈ K i
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedBall (r, y).2 (r, y).1 ⊆ 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i

Tactic:
apply mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
  (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)

Result:
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
⊢ {x_1 |
      x_1 ∈ Prod.snd ⁻¹' ⋂ i, ⋂ (_ : x ∉ K i), (K i)ᶜ →
        x_1 ∈
          {x_2 |
            x_2 ∈ {x_3 | (fun x_4 => ∀ i ∈ {b | x ∈ K b}, closedBall x_4.2 x_4.1 ⊆ U i) x_3} →
              x_2 ∈ {x | (fun p => ∀ (i : ι), p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i) x}}} ∈
    𝓝 0 ×ˢ 𝓝 x

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
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i

Tactic:
suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i by
  apply mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
    (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
  apply univ_mem'
  rintro ⟨r, y⟩ hxy hyU i hi
  simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
  exact hyU _ (hxy _ hi)

Result:
ι : 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
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i

Proof state:
case h
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
⊢ ∀ (a : ℝ≥0∞ × X),
    a ∈
      {x_1 |
        x_1 ∈ Prod.snd ⁻¹' ⋂ i, ⋂ (_ : x ∉ K i), (K i)ᶜ →
          x_1 ∈
            {x_2 |
              x_2 ∈ {x_3 | (fun x_4 => ∀ i ∈ {b | x ∈ K b}, closedBall x_4.2 x_4.1 ⊆ U i) x_3} →
                x_2 ∈ {x | (fun p => ∀ (i : ι), p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i) x}}}

Tactic:
rintro ⟨r, y⟩ hxy hyU i hi

Result:
case h.mk
ι : 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
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
r : ℝ≥0∞
y : X
hxy : (r, y) ∈ Prod.snd ⁻¹' ⋂ i, ⋂ (_ : x ∉ K i), (K i)ᶜ
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ i ∈ {b | x ∈ K b}, closedBall x_2.2 x_2.1 ⊆ U i) x_1}
i : ι
hi : (r, y).2 ∈ K i
⊢ closedBall (r, y).2 (r, y).1 ⊆ 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
i : ι
hi : x ∈ K i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i

Tactic:
rcases nhds_basis_closed_eball.mem_iff.1 ((hU i).mem_nhds <| hKU i hi) with ⟨R, hR₀, hR⟩

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
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i