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

State before:
X : Type
inst✝ : Norm X
f : ℕ → X
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖
Tactic:
have h := Filter.HasBasis.tendsto_iff (f := f) Filter.atTop_basis atInf_basis
State after:
X : Type
inst✝ : Norm X
f : ℕ → X
h : Tendsto f atTop atInf ↔ ∀ (ib : ℝ), True → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ {x | ib < ‖x‖}
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖

State before:
X : Type
inst✝ : Norm X
f : ℕ → X
h : Tendsto f atTop atInf ↔ ∀ (ib : ℝ), True → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ {x | ib < ‖x‖}
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖
Tactic:
simpa only [mem_Ici, ge_iff_le, mem_setOf_eq, exists_true_left, forall_true_left, true_and]
  using h
State after:
no goals