have := u_anti h_z_le_y
case intro.intro.intro.inr.inr.intro.intro
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) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_z_le_y : ↑z ≤ y
⊢ False
case intro.intro.intro.inr.inr.intro.intro
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) < ε
h3 : f y < u y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hzb : ↑z ∈ Metric.ball y δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_z_le_y : ↑z ≤ y
this : u y ≤ u ↑z
⊢ False