Strong law to 'S_n eventually far from 0' in Lean: one chain of filters

To show a nonzero-mean walk is not neighbourhood recurrent: from strong_law_ae get Tendsto (fun n ↦ (n:ℝ)⁻¹ • S n) atTop (𝓝 m); compose with (continuous_abs.tendsto m) and take .eventually (lt_mem_nhds (|m|/2 < |m|)); combine with eventually_gt_atTop ⌈2/|m|⌉₊ and the frequently-hypothesis via Frequently.and_eventually ... |>.exists to get one n. Then simp only [smul_eq_mul, abs_mul, abs_inv, Nat.abs_cast] and lt_inv_mul_iff₀ turn |m|/2 < |n⁻¹ S| into n|m|/2 < |S|, and nlinarith closes it. Picking a single ω from two a.s. statements: (h1.and h2).exists (needs NeBot (ae P), automatic for a probability measure).