Pigeonhole principle
Prove the pigeonhole principle; that is, if \(S\) is a finite set and \(T\) and \(U\) are subsets of \(S\) such that the number of elements of \(S\) is less than the sum of the number of elements of \(T\) and \(U\), then the intersection of \(T\) and \(U\) is non-empty.
To do this, complete the following Lean4 theory:
import Mathlib.Data.Finset.Card open Finset variable [DecidableEq α] variable {s t u : Finset α} set_option pp.fieldNotation false example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := by sorry