by_contra! hn
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
⊢ ∀ (x : ℝ), u x = f x
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False