awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a
have rw : ENNReal.ofReal (a - (a - r) / 2 + (a - r) / 2) = ENNReal.ofReal a
Tactic: rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a
have rw₁ : ENNReal.ofReal a = ENNReal.ofReal a
Tactic: rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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)) ≤ ε}
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have S_open : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
have this : oscillationWithin f D x < ε
Tactic: have : oscillationWithin f D x < ε := hK x hx
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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 < ε
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
have this₁ : ∃ (i : Set F) (_ : f ⁻¹' i ∈ 𝓝[D] x), ediam i < ε
Tactic: simp only [oscillationWithin, Filter.mem_map, iInf_lt_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 < ε
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
have obtain : ∀ (n : Set F) (hn₁ : f ⁻¹' n ∈ 𝓝[D] x) (hn₂ : ediam n < ε),
  Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
Tactic: obtain ⟨n, hn₁, hn₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 < ε
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
have obtain : ∀ (r : ℝ≥0∞) (r0 : r > 0) (hr : eball x r ∩ D ⊆ f ⁻¹' n), Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
Tactic: obtain ⟨r, r0, hr⟩ := EMetric.mem_nhdsWithin_iff.1 hn₁
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : r > 0), S r) x
have simp : ∃ (i : ℝ), 0 < i ∧ x ∈ S i
Tactic: simp only [gt_iff_lt, mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
have grw : ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam n
Tactic: grw [← hn₂, ← image_subset_iff.2 hr, hr']
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
have grw₁ : ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam (f '' (eball x r ∩ D))
Tactic: grw [← hn₂, ← image_subset_iff.2 hr, hr']
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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))
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
have grw₂ : ediam (f '' (eball x r ∩ D)) ≤ ediam (f '' (eball x r ∩ D))
Tactic: grw [← hn₂, ← image_subset_iff.2 hr, hr']
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have this : ∀ (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']
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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)) ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have pos : ∀ (r_top : r = ∞), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
Tactic: by_cases r_top : r = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have neg : ∀ (r_top : ¬r = ∞), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
Tactic: by_cases r_top : r = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
have neg : ∀ (r' : ℝ) (hr' : 0 < r' ∧ r' < r.toReal), ∃ (i : ℝ), 0 < i ∧ x ∈ S i
Tactic: obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 : ℝ
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have left : 0 < r'
Tactic: use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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₁ : ℝ
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have left₁ : r.toReal > r'
Tactic: use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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'
⊢ ∃ (i : ℝ), 0 < i ∧ x ∈ S i
have right : ediam (f '' (eball x (ENNReal.ofReal r.toReal) ∩ D)) ≤ ε
Tactic: use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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)
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have S_cover : 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
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have S_antitone : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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₁
⊢ ∃ r > 0, K ⊆ S r
have obtain : ∀ (T : Set ℝ) (Tb : T ⊆ Real.lt✝ 0) (Tfin : T.Finite) (hT : K ⊆ ⋃ i ∈ T, S i), ∃ r > 0, K ⊆ S r
Tactic: obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ∃ r > 0, K ⊆ S r
have pos : ∀ (T_nonempty : T.Nonempty), ∃ r > 0, K ⊆ S r
Tactic: by_cases T_nonempty : T.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ∃ r > 0, K ⊆ S r
have neg : ∀ (T_nonempty : ¬T.Nonempty), ∃ r > 0, K ⊆ S r
Tactic: by_cases T_nonempty : T.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ∃ r > 0, K ⊆ S r
have right : K ⊆ S (IsWF.min (s := T) sorry T_nonempty)
Tactic: use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)
have right : ∀ (r : ℝ) (hr : Membership.mem (γ := Set E) (⋃ (_ : r ∈ T), S r) x), x ∈ S (IsWF.min (s := T) sorry T_nonempty)
Tactic: obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ x ∈ S (IsWF.min (s := T) ⋯ T_nonempty)
have hr₁ : r ∈ T ∧ x ∈ S r
Tactic: simp only [mem_iUnion, exists_prop] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ ∃ r > 0, K ⊆ S r
have T_nonempty₁ : T = ∅
Tactic: rw [not_nonempty_iff_eq_empty] at T_nonempty
Cleared hypotheses: T_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 = ∅
⊢ ∃ r > 0, K ⊆ S r
have w : ℝ
Tactic: use 1, one_pos, subset_trans hT (by simp [T_nonempty])
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 : ℝ
⊢ ∃ r > 0, K ⊆ S r
have left : GT.gt (α := ℝ) 1 0
Tactic: use 1, one_pos, subset_trans hT (by simp [T_nonempty])
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ ∃ r > 0, K ⊆ S r
have right : K ⊆ S 1
Tactic: use 1, one_pos, subset_trans hT (by simp [T_nonempty])