awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hD : D ∈ 𝓝 x
rw : oscillationWithin f D x = ⨅ S ∈ Filter.map f (𝓝 x), ediam S
rw₁ : Eq (α := ℝ≥0∞) (⨅ S ∈ Filter.map f (𝓝[D] x), ediam S) (⨅ S ∈ Filter.map f (𝓝 x), ediam S)
rw₂ rw₃ : Eq (α := ℝ≥0∞) (⨅ S ∈ Filter.map f (𝓝 x), ediam S) (⨅ S ∈ Filter.map f (𝓝 x), ediam S)
⊢ oscillationWithin f D x = oscillation f x

Tactic:
rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]

Premises used: Iff.mpr, oscillation, nhdsWithin_eq_nhds, oscillationWithin
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
⊢ oscillationWithin f univ x = oscillation f x

Tactic:
oscillationWithin_nhds_eq_oscillation f univ x Filter.univ_mem

Premises used: Set.univ, oscillationWithin_nhds_eq_oscillation, Filter.univ_mem
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
rw : oscillationWithin f D x ≤ 0
⊢ oscillationWithin f D x = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
⊢ oscillationWithin f D x ≤ 0

Tactic:
_root_.le_of_forall_pos_le_add fun ε hε ↦ ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), oscillationWithin f D x ≤ 0 + ε
⊢ oscillationWithin f D x ≤ 0

Tactic:
refine _root_.le_of_forall_pos_le_add fun ε hε ↦ ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
rw : oscillationWithin f D x ≤ ε
⊢ oscillationWithin f D x ≤ 0 + ε

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : 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ε]

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)

Tactic:
have : eball (f x) (ε / 2) ∈ (𝓝[D] x).map f :=
    hf <| eball_mem_nhds _ (by simp [ne_of_gt hε])
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ oscillationWithin f D x ≤ ε

Tactic:
(biInf_le ediam this).trans (le_of_le_of_eq ediam_eball_le ?_)

Premises used: le_of_le_of_eq, Metric.ediam_eball_le, Metric.ediam, oscillationWithin, LE.le.trans, biInf_le
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
refine : 2 * (ε / 2) = ε
⊢ oscillationWithin f D x ≤ ε

Tactic:
refine (biInf_le ediam this).trans (le_of_le_of_eq ediam_eball_le ?_)

Premises used: le_of_le_of_eq, Metric.ediam_eball_le, Metric.ediam, LE.le.trans, biInf_le
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 * (ε / 2) = ε

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

Premises used: ENNReal.mul_div_cancel
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ ContinuousWithinAt f univ x

Tactic:
rw [← continuousWithinAt_univ f x] at hf

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
hf : ContinuousWithinAt f univ x
⊢ oscillation f x = 0

Tactic:
oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero

Premises used: Eq.rec, ContinuousWithinAt.oscillationWithin_eq_zero, oscillationWithin_univ_eq_oscillation
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
hf : ContinuousWithinAt f univ x
⊢ oscillation f x = 0

Tactic:
exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
⊢ oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x

Tactic:
⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩

Premises used: Iff.mpr, EMetric.tendsto_nhds, ContinuousWithinAt.oscillationWithin_eq_zero, Iff.intro
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
refine : ∀ (hf : oscillationWithin f D x = 0) (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
⊢ oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x

Tactic:
refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ (i : Set F) (_ : i ∈ Filter.map f (𝓝[D] x)), ediam i < ε

Tactic:
simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0

Premises used: iInf_lt_iff, oscillationWithin
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ∃ (i : Set F) (_ : i ∈ Filter.map f (𝓝[D] x)), ediam i < ε
obtain :
  ∀ (S : Set F) (hS : S ∈ Filter.map f (𝓝[D] x)) (Sε : ediam S < ε), ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
obtain ⟨S, hS, Sε⟩ := ε0
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : ediam S < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)

Premises used: lt_of_le_of_lt, Filter.Eventually, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : ediam S < ε
refine : ∀ (y : E) (hy : y ∈ f ⁻¹' S), edist (f y) (f x) ≤ ediam S
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)

Premises used: lt_of_le_of_lt, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : ediam S < ε
y : E
hy : y ∈ f ⁻¹' S
⊢ edist (f y) (f x) ≤ ediam S

Tactic:
edist_le_ediam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)

Premises used: Metric.edist_le_ediam_of_mem, mem_of_mem_nhdsWithin, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : ediam S < ε
y : E
hy : y ∈ f ⁻¹' S
⊢ edist (f y) (f x) ≤ ediam S

Tactic:
exact edist_le_ediam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)

Premises used: Metric.edist_le_ediam_of_mem, mem_of_mem_nhdsWithin, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
rw : oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x
⊢ oscillation f x = 0 ↔ ContinuousAt f x

Tactic:
rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]

Premises used: continuousWithinAt_univ, oscillationWithin_univ_eq_oscillation
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
⊢ oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x

Tactic:
OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)

Premises used: Set.mem_univ, OscillationWithin.eq_zero_iff_continuousWithinAt
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
⊢ oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x

Tactic:
exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)

Premises used: Set.mem_univ, OscillationWithin.eq_zero_iff_continuousWithinAt
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ENNReal.ofReal ((a - r) / 2) > 0

Tactic:
simp [ar]
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
refine :
  ∀ r > 0,
    ∀ x ∈ S r,
      ∀ (a : ℝ) (ar : a > r) (ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε),
        eball x (ENNReal.ofReal ((a - r) / 2)) ⊆ S r
⊢ ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)

Tactic:
refine fun r _ ↦ EMetric.isOpen_iff.mpr fun x ⟨a, ar, ha⟩ ↦
      ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
linarith : a - (a - r) / 2 ≤ r → 2 / 2 = 1
linarith₁ : a - (a - r) / 2 ≤ r → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a - (a - r) / 2 ≤ r → GT.gt (α := ℝ) 2 0
linarith₃ : a - (a - r) / 2 ≤ r → r - a + (2 * a - (1 * a - 1 * r) - 2 * r) = 0
⊢ a - (a - r) / 2 > r

Tactic:
linarith
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
refine :
  ∀ (y : E) (hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))) (z : E)
    (hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D), z ∈ eball x (ENNReal.ofReal a) ∩ D
⊢ eball x (ENNReal.ofReal ((a - r) / 2)) ⊆ S r

Tactic:
refine fun y hy ↦ ⟨a - (a - r) / 2, by linarith,
      le_trans (ediam_mono (image_mono fun z hz ↦ ?_)) ha⟩
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ z ∈ eball x (ENNReal.ofReal a) ∩ D

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

Premises used: lt_of_le_of_lt, Set.Mem, setOf, Set.inter, lt_of_lt_of_eq, And.right, And.left, And.intro, ENNReal.add_lt_add, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
refine : ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a
⊢ z ∈ eball 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⟩
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
linarith : a - (a - r) / 2 < 0 → 2 / 2 = 1
linarith₁ : a - (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a - (a - r) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : a - (a - r) / 2 < 0 → 2 * (0 - r) + (r - a) + (2 * a - (1 * a - 1 * r) - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : a - (a - r) / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ a - (a - r) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
linarith : (a - r) / 2 < 0 → 2 / 2 = 1
linarith₁ : (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (a - r) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (a - r) / 2 < 0 → r - a + (1 * a - 1 * r - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ (a - r) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
h : r > 0
x : E
h_1 : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
rw : ENNReal.ofReal (a - (a - r) / 2 + (a - r) / 2) = ENNReal.ofReal a
rw₁ rw₂ : ENNReal.ofReal a = ENNReal.ofReal a
⊢ 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]

Premises used: ENNReal.ofReal_add, sub_add_cancel
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
⊢ ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)

Tactic:
have S_open : ∀ r > 0, IsOpen (S r) := by
    refine fun r _ ↦ EMetric.isOpen_iff.mpr fun x ⟨a, ar, ha⟩ ↦
      ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩
    refine fun y hy ↦ ⟨a - (a - r) / 2, by linarith,
      le_trans (ediam_mono (image_mono fun z hz ↦ ?_)) ha⟩
    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⟩
    rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
⊢ oscillationWithin f D x < ε

Tactic:
have : oscillationWithin f D x < ε := hK x hx
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
this : oscillationWithin f D x < ε
⊢ ∃ (i : Set F) (_ : f ⁻¹' i ∈ 𝓝[D] x), ediam i < ε

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

Premises used: iInf_lt_iff, oscillationWithin, Filter.mem_map
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
this : ∃ (i : Set F) (_ : f ⁻¹' i ∈ 𝓝[D] x), ediam i < ε
obtain :
  ∀ (n : Set F) (hn₁ : f ⁻¹' n ∈ 𝓝[D] x) (hn₂ : ediam n < ε),
    Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := this
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
obtain :
  ∀ (r : ℝ≥0∞) (r0 : r > 0) (hr : eball x r ∩ D ⊆ f ⁻¹' n),
    Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x

Tactic:
obtain ⟨r, r0, hr⟩ := EMetric.mem_nhdsWithin_iff.1 hn₁

Premises used: Iff.mp, EMetric.mem_nhdsWithin_iff
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
simp : ∃ (i : ℝ), 0 < i ∧ x ∈ S i
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x

Tactic:
simp only [gt_iff_lt, mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, gt_iff_lt
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
r' : ℝ
hr' : ENNReal.ofReal r' ≤ r
grw : ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam n
grw₁ : ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam (f '' (eball x r ∩ D))
grw₂ grw₃ : ediam (f '' (eball x r ∩ D)) ≤ ediam (f '' (eball x r ∩ D))
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε

Tactic:
grw [← hn₂, ← image_subset_iff.2 hr, hr']

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
⊢ ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε

Tactic:
have : ∀ r', (ENNReal.ofReal r') ≤ r →
        ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε := by
      intro r' hr'
      grw [← hn₂, ← image_subset_iff.2 hr, hr']
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
pos : ∀ (r_top : r = ∞), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
neg : ∀ (r_top : ¬r = ∞), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i

Tactic:
by_cases r_top : r = ⊤