no goals
a b : ℝ
h : ↑a < ↑b
⊢ ∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b
simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]
no goals
a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ ↑a < ↑↑b
simpa using hab
no goals
a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑↑b < ↑a
simpa using hab