Witnessing convergence at a nonzero index

Stream: mathlib4

[Connor Gordon]

I'm sure this is simple, but I'm not great at using convergence of filters. I've reduced what I'm trying to prove down to

import Mathlib.Topology.MetricSpace.CantorScheme

example {u : ℕ → ENNReal} (hu : Filter.Tendsto u Filter.atTop (nhds 0)) :
  ∃ n : ℕ, u n.succ ≤ ε := by
    sorry

but I'm having trouble proving this. Could I get some help?

[Floris van Doorn]

Here is one way:

import Mathlib.Topology.MetricSpace.CantorScheme

open Filter ENNReal Topology Set
example {u : ℕ → ℝ≥0∞} (hu : Tendsto u atTop (𝓝 0)) {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ n : ℕ, u n.succ ≤ ε := by
  have h1 : Iic ε ∈ 𝓝 0 := by exact? says exact Iic_mem_nhds hε
  have h2 : ∀ᶠ (x : ℕ) in atTop, u x ∈ Iic ε := by exact? says exact hu.eventually_mem h1
  rw [eventually_atTop] at h2
  obtain ⟨n, hn⟩ := h2
  use n
  apply hn
  exact? says exact Nat.le.step Nat.le.refl

[Floris van Doorn]

Hopefully that generalizes to other problems you are interested in, and shows that you actually can make much stronger conclusions.

[Matt Diamond]

@Floris van Doorn I'm curious, is there a benefit to writing by exact? says exact Iic_mem_nhds hε instead of by exact Iic_mem_nhds hε? Is the idea to indicate to other readers where the result came from?

[Floris van Doorn]

Yes, it's just to show that Lean can do this itself by running exact?

[Patrick Massot]

import Mathlib.Topology.MetricSpace.CantorScheme

open Filter Topology Set

example {u : ℕ → ENNReal} (hu : Tendsto u atTop (nhds 0)) {ε : ENNReal}
    (ε_pos : 0 < ε) : ∃ n : ℕ, u n.succ ≤ ε := by
  rcases  eventually_atTop.mp <| eventually_le_of_tendsto_lt ε_pos hu with ⟨m, hm⟩
  exact ⟨m, hm _ m.le_succ⟩

[Matt Diamond]

it just seems kind of odd to see stuff like simp? says in the mathlib codebase... I would think we would use the suggestion itself

[llllvvuu]

In the case of simp it is helpful to have the original invocation since it is not immediately obvious from the output (i.e. what lemmas needed to be explicitly provided)