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

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