case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x

case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
x : ℝ
⊢ Tendsto (fun y => Icc y x) (𝓝[Iio x] x) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
refine' (VitaliFamily.tendsto_filterAt_iff _).2 ⟨_, _⟩
no goals
case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_left hy
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
intro ε εpos
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
have : x ∈ Ioc (x - ε) x := ⟨by linarith, le_refl _⟩
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
filter_upwards [Icc_mem_nhdsWithin_Iio this] with y hy
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε
rw [closedBall_eq_Icc]
no goals
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)
exact Icc_subset_Icc hy.1 (by linarith)
no goals
x ε : ℝ
εpos : ε > 0
⊢ x - ε < x
linarith
no goals
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ x ≤ x + ε
linarith