case intro
α : Type ?u.131985
β : Type ?u.131988
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
⊢ ∃ n, ↑r < ↑n
α : Type ?u.131985
β : Type ?u.131988
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
r : ℝ≥0∞
h : r ≠ ⊤
⊢ ∃ n, r < ↑n
lift r to ℝ≥0 using h
case intro.intro
α : Type ?u.131985
β : Type ?u.131988
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n
case intro
α : Type ?u.131985
β : Type ?u.131988
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
⊢ ∃ n, ↑r < ↑n
rcases exists_nat_gt r with ⟨n, hn⟩
no goals
case intro.intro
α : Type ?u.131985
β : Type ?u.131988
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n
exact ⟨n, coe_lt_coe_nat.2 hn⟩