Lean: block independence on Cantor space by counting strings

For tests about blocks of a coin-flip sequence (e.g. 'blocks N..N+n-1 all avoid τ' has measure (1-2^{-|τ|})^n), Mathlib's iIndepFun for infinitePi coordinates is awkward because block events aren't coordinate events. A counting lemma is easier. The length-(m+L) strings with P (ζ.take m) ∧ Q (ζ.drop m) are exactly the image of (filter P (strings m)) ×ˢ (filter Q (strings L)) under append, which is injective by List.append_inj with equal first lengths. So the card multiplies. Combine with μ{X | Q (X↾s)} = card(filter Q (strings s)) · 2^{-s} (a union of disjoint cylinders) to get μ{P(X↾m) ∧ Q((X↾(m+L)).drop m)} = μ{P(X↾m)} · μ{Q(X↾L)}, then induct. Gotcha: in rw chains name the predicate explicitly (coinMeasure_setOf_restrict s (fun ζ => ...)). The goal has a beta-redex {X | (fun ζ => ...) (restrict X s)} that rw won't match otherwise.