theorem TetrahedronFreeHypergraph.card_five_supersets {n : ℕ} (e : Finset (Fin n)) (he : e.card = 3) : {S ∈ Finset.powersetCard 5 Finset.univ | e ⊆ S}.card = (n - 3).choose 2

For a fixed $3$-element set $e \subseteq \mathrm{Fin}\,n$, the number of $5$-element supersets of $e$ equals $\binom{n-3}{2}$, since one chooses the $2$ additional vertices from the remaining $n-3$.

theorem TetrahedronFreeHypergraph.card_four_in_five {n : ℕ} (S : Finset (Fin n)) (hS : S.card = 5) (e : Finset (Fin n)) (he : e.card = 3) (heS : e ⊆ S) : {T ∈ Finset.powersetCard 4 S | e ⊆ T}.card = 2

Inside a $5$-element set $S$, a fixed $3$-element subset $e \subseteq S$ is contained in exactly $2$ of the $4$-element subsets of $S$ (corresponding to the $2$ elements of $S \setminus e$ one can adjoin to form a $4$-set).

theorem TetrahedronFreeHypergraph.five_set_edges_le_seven {n : ℕ} (E : Finset (Finset (Fin n))) (hUnif : ∀ e ∈ E, e.card = 3) (hFree : ∀ S ∈ Finset.powersetCard 4 Finset.univ, {x ∈ Finset.powersetCard 3 S | x ∈ E}.card ≤ 3) (S : Finset (Fin n)) (hS : S ∈ Finset.powersetCard 5 Finset.univ) : {x ∈ E | x ⊆ S}.card ≤ 7

Lemma 2.4.3. Any $5$-vertex tetrahedron-free $3$-uniform hypergraph has at most $7$ hyperedges. Equivalently, for every $5$-set $S$ at most $7$ hyperedges of $E$ lie inside $S$. Proved by double counting pairs (hyperedge, $4$-superset).

theorem TetrahedronFreeHypergraph.improved_sampling_bound {n : ℕ} (hn : 5 ≤ n) (E : Finset (Finset (Fin n))) (hUnif : ∀ e ∈ E, e.card = 3) (hFree : ∀ S ∈ Finset.powersetCard 4 Finset.univ, {x ∈ Finset.powersetCard 3 S | x ∈ E}.card ≤ 3) : 10 * E.card ≤ 7 * n.choose 3

Improved sampling bound (Proposition 2.4.4). A tetrahedron-free $3$-uniform hypergraph on $n \geq 5$ vertices has at most $\tfrac{7}{10}\binom{n}{3}$ hyperedges; equivalently $10 |E| \leq 7 \binom{n}{3}$. The proof samples random $5$-sets and applies Lemma 2.4.3.