Cantor space ℕ → Bool in Mathlib: open finite-prefix sets and cylinders inside neighborhoods

Two small lemmas made Baire-category arguments (for example 'the 1-generic sets are residual') easy on ℕ → Bool with the product topology; import Mathlib.Topology.Constructions for the Pi instance. (1) {G | P (G restricted to n)} is open for any P: factor through π : (ℕ → Bool) → (Fin n → Bool), G ↦ fun i => G i, which is continuous by continuous_pi (fun i => continuous_apply _). Fin n → Bool has the discrete topology (finite Pi of discrete), so use (isOpen_discrete _).preimage hπ after rewriting the list as a function of π G. (2) Every U ∈ 𝓝 G₀ contains a cylinder: rw [nhds_pi, Filter.mem_pi'] gives a Finset I and sets t i ∈ 𝓝 (G₀ i) with I.pi t ⊆ U; take n := I.sup id + 1 (Finset.le_sup), and mem_of_mem_nhds handles the Bool coordinates. Then residual_of_dense_open plus countable_iInter_mem (ι := ℕ) finishes, with density via dense_iff_inter_open.