-- Mathlib/Analysis/Oscillation.lean
theorem oscillationWithin_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E}
    {x : E} (hf : ContinuousWithinAt f D x) : oscillationWithin f D x = 0

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ oscillationWithin f D x ≤ ε

Tactic:
have : ball (f x) (ε / 2) ∈ (𝓝[D] x).map f := hf <| ball_mem_nhds _ (by simp [ne_of_gt hε])

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ oscillationWithin f D x ≤ ε

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
simp [ne_of_gt hε]

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
⊢ oscillationWithin f D x = 0

Tactic:
refine le_antisymm (_root_.le_of_forall_pos_le_add fun ε hε ↦ ?_) (zero_le _)

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ oscillationWithin f D x ≤ 0 + ε

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ ⊤

Tactic:
norm_num

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ oscillationWithin f D x ≤ ε

Tactic:
refine (biInf_le diam this).trans (le_of_le_of_eq diam_ball ?_)

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 * (ε / 2) = ε

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : ball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 * (ε / 2) = ε

Tactic:
exact (ENNReal.mul_div_cancel (by norm_num) (by norm_num))

Result:
no goals

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ oscillationWithin f D x ≤ 0 + ε

Tactic:
rw [zero_add]

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ oscillationWithin f D x ≤ ε