case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε
cases' exists_nat_gt (1 / ε) with n hn
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
use n
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1

case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε
rw [div_lt_iff, ← div_lt_iff' hε]
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1
apply hn.trans
no goals
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1
simp [zero_lt_one]
no goals
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1
exact n.cast_add_one_pos