r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
r : ℝ
⊢ ¬Infinite ↑r
rw [not_infinite_iff_exist_lt_gt]
no goals
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩