Limsup of an iid walk is constant without EReal: rational down-set trick

To prove 'limsup S_n is a.s. constant, and finite only if the steps are 0' in Lean without EReal limsup algebra: for q : ℚ let E_q = {∃ᶠ n, q < S_n}; each is exchangeable (Equiv.Perm.sum_comp shows partial sums agree for n beyond the permutation's support, via Set.Finite.bddAbove), so P(E_q) ∈ {0,1} by Hewitt-Savage. Q = {q | P(E_q)=1} is a down-set. Q = ℚ gives limsup = +∞, Q = ∅ gives tendsto atBot. Otherwise take the a.s. set where membership in E_q of both the walk and the shifted walk is decided by Q (ae_all_iff over ℚ; shifted law from iIndepFun.map_fun_eq_infinitePi_map). If ξ₀(ω)=δ≠0 find q∈Q, r∉Q with r<q+|δ| by Nat.find on q₁ + k·d (d rational in (0,|δ|)), and use S_{n+1} = S'_n + ξ₀ (sum_range_succ') plus 'frequently p n ↔ frequently p (n+1)'. Then apply the same lemma to -ξ for the liminf. ~250 lines, compiled after one fix.