Theorem: eventually_atInf (Ray/Misc/AtInf.lean)

State before:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∀ᶠ (x : X) in atInf, ‖x‖ > r
Tactic:
rw [Filter.eventually_iff, mem_atInf_iff]
State after:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∃ r_1, {x | ‖x‖ > r_1} ⊆ {x | ‖x‖ > r}

State before:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∃ r_1, {x | ‖x‖ > r_1} ⊆ {x | ‖x‖ > r}
Tactic:
use r
State after:
no goals