have : ∃ z : ℚ, y < z ∧ dist (z:ℝ) y < δ := by
  have hyδ : y < y + δ := lt_add_of_pos_right y hδ0
  obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
  refine ⟨z, hz1, ?_⟩
  . rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
    exact sub_left_lt_of_lt_add hz2
case intro.intro.intro.inl
u f : ℝ → ℝ
u_anti : Antitone 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) < ε
h1 : u y < f y
⊢ False
case intro.intro.intro.inl
u f : ℝ → ℝ
u_anti : Antitone 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) < ε
h1 : u y < f y
this : ∃ z, y < ↑z ∧ dist (↑z) y < δ
⊢ False