Direct diagonal bounded capture, without a sunflower extraction.

theorem GenLimit.FiniteWitness.Simplified.bounded_capture {α : Type u_1} (d : ℕ) (U : ℕ → Finset α) (hU : ∀ (n : ℕ), (U n).card ≤ d) (C : ℕ → Set α) : ∃ (D : Set α), {n : ℕ | ↑(U n) ⊆ D}.Infinite ∧ ∀ (m : ℕ), (C m).Infinite → ¬C m ⊆ D

Exact bounded-capture statement, proved by direct diagonal selection.

theorem GenLimit.FiniteWitness.Simplified.bounded_capture_indexed {α : Type u_1} {ι : Type u_2} [Countable ι] (d : ℕ) (U : ℕ → Finset α) (hU : ∀ (n : ℕ), (U n).card ≤ d) (C : ι → Set α) : ∃ (D : Set α), {n : ℕ | ↑(U n) ⊆ D}.Infinite ∧ ∀ (i : ι), (C i).Infinite → ¬C i ⊆ D