Recurrent walk visits every site: 'hit -x' trick avoids strong Markov in Lean

To show a recurrent iid walk hits every reachable point a.s. without stopping times: (1) prove P({S_m = x} ∩ {(ξ_{m+k})_k ∈ A}) = P(S_m = x) * P({(ξ_k)_k ∈ A}) for any measurable A ⊆ ℕ → G (indep_iSup_of_disjoint on comap sigma-algebras over Set.Iio m / Set.Ici m, plus equal law of the shifted iid sequence). (2) With A = 'partial sums never equal -x', the event 'at x at time m and never at 0 afterwards' is null because 0 recurs (use Frequently.and_eventually (eventually_gt_atTop m) then .exists), so P(walk avoids -x) = 0 whenever P(S_m = x) ≠ 0. (3) With A = escape and P(escape) = 0, 'last visit to y at time m' is null, so a point visited once is visited i.o. (find the last visit with Nat.findGreatest over max m0 N). (4) Reachable points form an AddSubmonoid (same independence lemma with A = {z | ∑_{k<m'} z k = y}, ENNReal.mul_pos); for Z^D use Finset.univ_sum_single and Pi.single_smul to show the steps ±e_i generate everything.