awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
have h : ∀ (t : ℝ) (x : E),
  v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a) ↔
    IsIntegralCurveAt γ v t₀
have refine : ∀
  (hγ :
    IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)),
  IsIntegralCurveAt γ v t₀
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul_ne_zero ha⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
⊢ IsIntegralCurveAt γ v t₀
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
⊢ IsIntegralCurveAt γ v t₀
have h₁ : v = HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ :
  v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
⊢ IsIntegralCurveAt γ v t₀
have h₂ : t₀ = t₀ / a / a⁻¹
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
have h : ∀ (t : ℝ) (x : E),
  v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
a : ℝ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
have rw : ∀ (hγ : IsIntegralCurveOn γ v univ) (a : ℝ),
  IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) univ
Tactic: rw [← isIntegralCurveOn_univ] at *
Cleared hypotheses: hγ, a
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) ↔
    IsIntegralCurve γ v
have refine : ∀ (hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))),
  IsIntegralCurve γ v
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
⊢ IsIntegralCurve γ v
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
⊢ IsIntegralCurve γ v
have h₁ : v = HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
have h : ∀ (t : ℝ) (x : E),
  v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ oscillationWithin f D x = oscillation f x
have rw : oscillationWithin f D x = ⨅ S ∈ Filter.map f (𝓝 x), ediam S
Tactic: rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
⊢ oscillationWithin f D x = oscillation f x
have rw₁ : Eq (α := ℝ≥0∞) (⨅ S ∈ Filter.map f (𝓝[D] x), ediam S) (⨅ S ∈ Filter.map f (𝓝 x), ediam S)
Tactic: rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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)
⊢ oscillationWithin f D x = oscillation f x
have rw₂ : Eq (α := ℝ≥0∞) (⨅ S ∈ Filter.map f (𝓝 x), ediam S) (⨅ S ∈ Filter.map f (𝓝 x), ediam S)
Tactic: rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
have rw : oscillationWithin f D x ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), oscillationWithin f D x ≤ 0 + ε
Tactic: refine _root_.le_of_forall_pos_le_add fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 < ε
⊢ oscillationWithin f D x ≤ 0 + ε
have rw : oscillationWithin f D x ≤ ε
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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 < ε
⊢ oscillationWithin f D x ≤ ε
have this : 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ε])
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 ≤ ε
have refine : 2 * (ε / 2) = ε
Tactic: refine (biInf_le ediam this).trans (le_of_le_of_eq ediam_eball_le ?_)
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ oscillation f x = 0
have hf₁ : ContinuousWithinAt f univ x
Tactic: rw [← continuousWithinAt_univ f x] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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
have refine : ∀ (hf : oscillationWithin f D x = 0) (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
Tactic: refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
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
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
have ε0₁ : ∃ (i : Set F) (_ : i ∈ Filter.map f (𝓝[D] x)), ediam i < ε
Tactic: simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0
Cleared hypotheses: ε0
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
have 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) < ε
Tactic: obtain ⟨S, hS, Sε⟩ := ε0
Cleared hypotheses: ε0
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
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) < ε
have refine : ∀ (y : E) (hy : y ∈ f ⁻¹' S), edist (f y) (f x) ≤ ediam S
Tactic: refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : TopologicalSpace E
f : E → F
x : E
⊢ oscillation f x = 0 ↔ ContinuousAt f x
have rw : oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x
Tactic: rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]
-- 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 > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
have 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
Tactic: refine fun r _ ↦ EMetric.isOpen_iff.mpr fun x ⟨a, ar, ha⟩ ↦
      ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩
-- 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))
⊢ a - (a - r) / 2 > r
have linarith : a - (a - r) / 2 ≤ r → 2 / 2 = 1
Tactic: linarith
-- 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))
linarith : a - (a - r) / 2 ≤ r → 2 / 2 = 1
⊢ a - (a - r) / 2 > r
have linarith₁ : a - (a - r) / 2 ≤ r → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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))
linarith : a - (a - r) / 2 ≤ r → 2 / 2 = 1
linarith₁ : a - (a - r) / 2 ≤ r → HMul.hMul (α := ℝ) 1 2 = 2
⊢ a - (a - r) / 2 > r
have linarith₂ : a - (a - r) / 2 ≤ r → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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))
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
⊢ a - (a - r) / 2 > r
have linarith₃ : a - (a - r) / 2 ≤ r → r - a + (2 * a - (1 * a - 1 * r) - 2 * r) = 0
Tactic: linarith
-- 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)) ≤ ε
⊢ eball x (ENNReal.ofReal ((a - r) / 2)) ⊆ S r
have 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
Tactic: refine fun y hy ↦ ⟨a - (a - r) / 2, by linarith,
      le_trans (ediam_mono (image_mono fun z hz ↦ ?_)) 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)) ≤ ε}
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
have refine : ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a
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⟩
-- 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
⊢ 0 ≤ a - (a - r) / 2
have linarith : a - (a - r) / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- 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
linarith : a - (a - r) / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ a - (a - r) / 2
have linarith₁ : a - (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
linarith : a - (a - r) / 2 < 0 → 2 / 2 = 1
linarith₁ : a - (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ a - (a - r) / 2
have linarith₂ : a - (a - r) / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
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
⊢ 0 ≤ a - (a - r) / 2
have linarith₃ : a - (a - r) / 2 < 0 → 2 * (0 - r) + (r - a) + (2 * a - (1 * a - 1 * r) - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- 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
⊢ 0 ≤ (a - r) / 2
have linarith : (a - r) / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- 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
linarith : (a - r) / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ (a - r) / 2
have linarith₁ : (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
linarith : (a - r) / 2 < 0 → 2 / 2 = 1
linarith₁ : (a - r) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ (a - r) / 2
have linarith₂ : (a - r) / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
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
⊢ 0 ≤ (a - r) / 2
have linarith₃ : (a - r) / 2 < 0 → r - a + (1 * a - 1 * r - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith