-- Mathlib/Analysis/Oscillation.lean
theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
    ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Proof state:
case intro.intro.intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : diam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : ball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → diam (f '' (ball x (ENNReal.ofReal r') ∩ D)) ≤ ε
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
by_cases r_top : r = ⊤

Result:
case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : diam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : ball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → diam (f '' (ball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : r = ⊤
⊢ ∃ i, 0 < i ∧ x ∈ S i

case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : diam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : ball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → diam (f '' (ball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ⊤
⊢ ∃ i, 0 < i ∧ x ∈ S i

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ ball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ ball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a

Tactic:
rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ ball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ ball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ z ∈ ball x (ENNReal.ofReal a) ∩ D

Tactic:
refine ⟨lt_of_le_of_lt (edist_triangle z y x) (lt_of_lt_of_eq (ENNReal.add_lt_add hz.1 hy) ?_),
  hz.2⟩

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ ball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ ball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ ball x (ENNReal.ofReal ((a - r) / 2))
⊢ a - (a - r) / 2 > r

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ ball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ ball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ 0 ≤ a - (a - r) / 2

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
x : E
hx : x ∈ K
this : oscillationWithin f D x < ε
⊢ x ∈ ⋃ r, ⋃ (_ : r > 0), S r

Tactic:
simp only [oscillationWithin, Filter.mem_map, iInf_lt_iff] at this

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
x : E
hx : x ∈ K
this : ∃ i, ∃ (_ : f ⁻¹' i ∈ 𝓝[D] x), diam i < ε
⊢ x ∈ ⋃ r, ⋃ (_ : r > 0), S r

Proof state:
case intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
⊢ ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
use δ, δ0

Result:
case right
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
⊢ ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Proof state:
case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T = ∅
⊢ ∃ r > 0, K ⊆ S r

Tactic:
use 1, one_pos, subset_trans hT (by simp [T_nonempty])

Result:
no goals