rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ dist (↑z) y < δ
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ ↑z - y < δ