obtain h5 | h6 := em (f y < u z)
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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
case inl
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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h5 : f y < u ↑z
⊢ u y < u ↑z

case inr
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) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
⊢ u y < u ↑z