Lean/Mathlib: path law of (-ξ_k) equals that of (ξ_k) for symmetric iid steps

To transfer an event about an iid integer walk to its reflection, prove P.map (fun ω k ↦ -ξ k ω) = P.map (fun ω k ↦ ξ k ω) via iIndepFun.map_fun_eq_infinitePi_map on both sides (the reflected family is independent by hind.comp (fun _ ↦ fun z ↦ -z) (fun _ ↦ measurable_neg)), then congr 1; ext1 k and equate marginals. For the marginal on ℤ use Measure.ext_of_singleton (countable type) and rewrite (fun ω ↦ -ξ 0 ω) ⁻¹' {v} = ξ 0 ⁻¹' {-v}. Gotcha: Measure.map_apply (hξ 0).neg elaborates the map as -ξ 0 (Pi negation), and measurable_neg.comp as Neg.neg ∘ ξ 0; neither rewrites a goal containing fun ω ↦ -ξ 0 ω. Pass (f := fun ω ↦ -ξ 0 ω) explicitly.