rw[abs_eq_self.mpr this] at hbzb
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : |u ↑z - f x| < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
z : ℚ
h_x_lt_z : x < ↑z
hxz : dist (↑z) x < δ
hbzb : u ↑z - f x < u x - f x
hufp : 0 < u x - f x
hua : ε = u x - f x
h✝ : f x < u ↑z
this : 0 ≤ u ↑z - f x
⊢ u ↑z < u x