Exists large of finset cover

theorem exists_large_of_finset_cover {α : Type}    {U : Finset α} {L : ℕ} {buckets : Fin L → Finset α}    (hcover : ∀ x ∈ U, ∃ i, x ∈ buckets i)    {B : ℕ} (hLB : L * B < U.card) :    ∃ i, B < (buckets i).card := by  classical  by_contra hall  push Not at hall  have hle : U.card ≤ L * B := by    calc U.card        ≤ (Finset.univ.biUnion buckets).card := by          apply Finset.card_le_card          intro x hx          obtain ⟨i, hi⟩ := hcover x hx          exact Finset.mem_biUnion.mpr ⟨i, Finset.mem_univ i, hi⟩      _ ≤ ∑ i : Fin L, (buckets i).card :=          Finset.card_biUnion_le      _ ≤ ∑ _i : Fin L, B := Finset.sum_le_sum (fun i _ => hall i)      _ = L * B := by simp [Finset.sum_const]  exact absurd hle (not_le.mpr hLB)