Erdős Problem 776

### What is the conjecture

https://www.erdosproblems.com/776

Let $r\geq 2$ and $A_1,\ldots,A_m\subseteq \\{1,\ldots,n\\}$ be such that $A_i\not\subseteq A_j$ for all $i\neq j$ and for any $t$ if there exists some $i$ with $\lvert A_i\rvert=t$ then there must exist at least $r$ sets of that size.

How large must $n$ be (as a function of $r$) to ensure that there is such a family which achieves $n-3$ distinct sizes of sets?

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start with the conjecture statement at https://www.erdosproblems.com/776 and review the repository's existing formalized conjectures to find the appropriate Lean entry point. Done means adding a complete formal statement of Erdős Problem 776 that matches the linked conjecture and fits the project's conventions.

Written by the indexing model from the issue text.