obtain ⟨y, hy⟩ := hn
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False
case intro
u f : ℝ → ℝ
u_anti : Antitone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
⊢ False