2026-02-20 A Lean Proof that \( \bigcup \left( \mathcal{F} \cap \mathcal{G} \right) \subseteq \bigcup \mathcal{F} \cap \bigcup \mathcal{G} \)