Forcing and independence

In Cohen forcing $\mathrm{Fn}(\omega, 2)$ (finite partial functions, stronger = larger), which of these sets are dense? Choose all that apply.

How many conditions does $\mathrm{Fn}(3, 2)$ have, i.e. how many partial functions from $\{0, 1, 2\}$ to $\{0, 1\}$ are there (including the empty function $\mathbb 1$)?

Why does the classical presentation of forcing start from a countable transitive model $M$?

In the proof that an $M$-generic filter $G$ (for a forcing in which every condition has two incompatible extensions) is not in $M$, which dense set does $G$ fail to meet if $G \in M$?

The proof that $\mathrm{Fn}(I, 2)$ has the countable chain condition takes uncountably many conditions $p_\xi$. What is the key step?

Assuming ZFC is consistent, which of these statements are independent of ZFC? Choose all that apply.

The Lean file orders Cohen conditions by extension: p ≤ q means q extends p. In this order, what does Mathlib's Order.Ideal Cohen correspond to in forcing?

The theorem no_filter_meets_every_dense (G : Order.Ideal Cohen) : ∃ D : Set Cohen, IsCofinal D ∧ ∀ p ∈ D, p ∉ G is proved with which witness D?

Write escape(reals, n): given a list of reals (functions from naturals to $\{0, 1\}$) and $n$, return a tuple of bits $p$ of length at least $n$ that disagrees with every listed real at some position. This is the Rasiowa–Sikorski construction for the dense sets 'decide bit $k$' ($k \lt n$) and 'disagree with $x$'.