The sunflower conjecture

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem CB002 — The sunflower conjecture

Does a bounded number of k-element sets force three of them to overlap in exactly the same core?

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : ∃ C : ℕ, ∀ (k : ℕ) (F : Finset (Finset ℕ)), ... := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.CB002.Statement

namespace Submission

theorem solution : Conjectura.CB002.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### sunflower

A sunflower is a family of sets any two of which meet in the same common core. The sunflower lemma, and the conjecture on how few sets force one to appear, are central to extremal set theory and to circuit lower bounds.

```lean
Conjectura.Combinatorics.IsSunflower
-- unfolds to:
def IsSunflower {α : Type*} [DecidableEq α]
    (F : Finset (Finset α)) (core : Finset α) : Prop :=
  ∀ A ∈ F, ∀ B ∈ F, A ≠ B → A ∩ B = core
```
Defined in this corpus.

### Finset

structure

```lean
Finset
```
Defined in Mathlib.

### card

theorem

```lean
A.card
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.