awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ≤ ε
r_top : r = ∞
⊢ GT.gt (α := ℝ) 2 1

Tactic:
simp
-- 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)) ≤ ε
r_top : r = ∞
⊢ ENNReal.ofReal 2 ≤ r

Tactic:
simp only [r_top, le_top]

Premises used: le_top
-- 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)) ≤ ε
r_top : r = ∞
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i

Tactic:
exact ⟨1, one_pos, 2, by simp, this 2 (by simp only [r_top, le_top])⟩
-- 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)) ≤ ε
r_top : ¬r = ∞
neg : ∀ (r' : ℝ) (hr' : 0 < r' ∧ r' < r.toReal), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i

Tactic:
obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)

Premises used: ne_of_gt, exists_between, ENNReal.toReal_pos
-- 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)) ≤ ε
r_top : ¬r = ∞
r' : ℝ
hr' : 0 < r' ∧ r' < r.toReal
w : ℝ
left : 0 < r'
w₁ : ℝ
left₁ : r.toReal > r'
right : ediam (f '' (eball x (ENNReal.ofReal r.toReal) ∩ D)) ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i

Tactic:
use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le

Premises used: ENNReal.ofReal_toReal_le, ENNReal.toReal, And.right, And.left
-- 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)
⊢ K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r

Tactic:
have S_cover : K ⊆ ⋃ r > 0, S r := by
    intro x hx
    have : oscillationWithin f D x < ε := hK x hx
    simp only [oscillationWithin, Filter.mem_map, iInf_lt_iff] at this
    obtain ⟨n, hn₁, hn₂⟩ := this
    obtain ⟨r, r0, hr⟩ := EMetric.mem_nhdsWithin_iff.1 hn₁
    simp only [gt_iff_lt, mem_iUnion, exists_prop]
    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']
    by_cases r_top : r = ⊤
    · exact ⟨1, one_pos, 2, by simp, this 2 (by simp only [r_top, le_top])⟩
    · obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
      use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
-- 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)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
⊢ ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁

Tactic:
have S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁ :=
    fun r₁ r₂ hr x ⟨a, ar₂, ha⟩ ↦ ⟨a, lt_of_le_of_lt hr ar₂, 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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
obtain : ∀ (T : Set ℝ) (Tb : T ⊆ Real.lt✝ 0) (Tfin : T.Finite) (hT : K ⊆ ⋃ i ∈ T, S i), ∃ r > 0, K ⊆ S r
⊢ ∃ r > 0, K ⊆ S r

Tactic:
obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover

Premises used: IsCompact.elim_finite_subcover_image
-- 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)
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
pos : ∀ (T_nonempty : T.Nonempty), ∃ r > 0, K ⊆ S r
neg : ∀ (T_nonempty : ¬T.Nonempty), ∃ r > 0, K ⊆ S r
⊢ ∃ r > 0, K ⊆ S r

Tactic:
by_cases T_nonempty : T.Nonempty

Premises used: Set.Nonempty
-- 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)
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.Nonempty
right : K ⊆ S (IsWF.min (s := T) ⋯ T_nonempty)
⊢ ∃ r > 0, K ⊆ S r

Tactic:
use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)

Premises used: Set.IsWF.min_mem, Set.IsWF.min, Set.Finite.isWF
-- 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)
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.Nonempty
x : E
hx : x ∈ K
right : ∀ (r : ℝ) (hr : Membership.mem (γ := Set E) (⋃ (_ : r ∈ T), S r) x), x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)
⊢ x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)

Tactic:
obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)

Premises used: Set.mem_iUnion, Iff.mp
-- 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)
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.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : Membership.mem (γ := Set E) (⋃ (_ : r ∈ T), S r) x
⊢ r ∈ T ∧ x ∈ S r

Tactic:
simp only [mem_iUnion, exists_prop] at hr

Premises used: Set.mem_iUnion, exists_prop
-- 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)
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.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : r ∈ T ∧ x ∈ S r
⊢ x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)

Tactic:
(S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2

Premises used: Set.Mem, setOf, And.right, And.left, Set.Finite.isWF, Set.IsWF.min_le
-- 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)
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.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : r ∈ T ∧ x ∈ S r
⊢ x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)

Tactic:
exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2

Premises used: And.right, And.left, Set.Finite.isWF, Set.IsWF.min_le
-- 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)
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.Nonempty
⊢ T = ∅

Tactic:
rw [not_nonempty_iff_eq_empty] at T_nonempty

Premises used: Set.not_nonempty_iff_eq_empty
-- 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)
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 = ∅
⊢ ⋃ i ∈ T, S i ⊆ S 1

Tactic:
simp [T_nonempty]
-- 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)
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 = ∅
w : ℝ
left : GT.gt (α := ℝ) 1 0
right : K ⊆ S 1
⊢ ∃ r > 0, K ⊆ S r

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

Premises used: subset_trans, one_pos
-- 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)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
obtain : ∀ (δ : ℝ) (δ0 : δ > 0) (hδ : K ⊆ S δ), ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
obtain ⟨δ, δ0, hδ⟩ : ∃ r > 0, K ⊆ S r := by
    obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
    by_cases T_nonempty : T.Nonempty
    · use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2
    · rw [not_nonempty_iff_eq_empty] at T_nonempty
      use 1, one_pos, subset_trans hT (by simp [T_nonempty])
-- 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)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
right : ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
use δ, δ0
-- 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)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
right :
  ∀ (a : ℝ) (δa : a > δ) (ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε),
    ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
obtain ⟨a, δa, ha⟩ := hδ xK
-- 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)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
a : ℝ
δa : a > δ
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
right : ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D))
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
grw [← 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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (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 : E
xK : x ∈ K
a : ℝ
δa : a > δ
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillation f x < ε
⊢ ∀ x ∈ K, oscillationWithin f univ x < ε

Tactic:
simp only [← oscillationWithin_univ_eq_oscillation] at hK

Premises used: oscillationWithin_univ_eq_oscillation
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ univ)) ≤ ε

Tactic:
comp.uniform_oscillationWithin hK

Premises used: IsCompact.uniform_oscillationWithin
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
h : ∀ (x : ℝ), ∀ a ∈ K, eball a (ENNReal.ofReal x) ∩ univ = eball a (ENNReal.ofReal x)
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' eball x (ENNReal.ofReal δ)) ≤ ε

Tactic:
convert! ← comp.uniform_oscillationWithin hK

Premises used: IsCompact.uniform_oscillationWithin
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
x : ℝ
a : E
h : a ∈ K
⊢ eball a (ENNReal.ofReal x) ∩ univ = eball a (ENNReal.ofReal x)

Tactic:
inter_univ _

Premises used: Set.inter_univ
-- Module: Mathlib.Analysis.Oscillation
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
x : ℝ
a : E
h : a ∈ K
⊢ eball a (ENNReal.ofReal x) ∩ univ = eball a (ENNReal.ofReal x)

Tactic:
exact inter_univ _

Premises used: Set.inter_univ
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u 0), f k) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u k))

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
rw :
  HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)
n₁ : ℕ
hmn : u 0 ≤ u n
hnk : u n ≤ u (n + 1)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))

Tactic:
rw [sum_range_succ, ← sum_Ico_consecutive]

Premises used: Finset.sum_Ico_consecutive, Finset.sum_range_succ
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)

Tactic:
add_le_add ihn this

Premises used: add_le_add
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)

Tactic:
exact add_le_add ihn this

Premises used: add_le_add
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ u 0 ≤ u n

Tactic:
hu n.zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ u n ≤ u (n + 1)

Tactic:
hu n.le_succ

Premises used: Nat.le_succ
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ u 0 ≤ u n

Tactic:
exacts [hu n.zero_le, hu n.le_succ]

Premises used: Nat.zero_le, Nat.le_succ