Intersection is nonempty of sum of card gt than univ card

Stream: Is there code for X?

[Christoph Spiegel]

Hey, does anything like this already exist in mathlib? I wasn't able to find it:

import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Card
import Mathlib.Tactic

variable {α : Type*} [Fintype α] [DecidableEq α] {S T : Finset α}

lemma card_add_le_inter_add_card_univ (S T : Finset α) : S.card + T.card ≤ (S ∩ T).card + Fintype.card α := by
  have := Finset.card_inter_add_card_union S T
  have := Finset.card_le_univ (S ∪ T)
  linarith

lemma inter_ne_empty_of_card_add_gt_card_univ (h : S.card + T.card > Fintype.card α) : (S ∩ T).Nonempty :=
  Finset.card_pos.mp (Nat.lt_add_left_iff_pos.mp (Nat.lt_of_lt_of_le h (card_add_le_inter_add_card_univ S T)))

lemma exists_ne_mem_inter_of_card_add_gt_card_univ (h : S.card + T.card > Fintype.card α) : ∃ x, x ∈ S ∩ T :=
  inter_ne_empty_of_card_add_gt_card_univ h

lemma exists_ne_mem_of_card_add_gt_card_univ (h : S.card + T.card > Fintype.card α) : ∃ x, x ∈ S ∧ x ∈ T := by
  obtain ⟨x, hx⟩ := exists_ne_mem_inter_of_card_add_gt_card_univ h
  exact ⟨x, Finset.mem_inter.mp hx⟩

[Yaël Dillies]

Yes, see docs#Finset.inter_nonempty_of_card_lt_card_add_card

[Yaël Dillies]

import Mathlib.Data.Fintype.Card

variable {α : Type*} [Fintype α] [DecidableEq α] {S T : Finset α}

namespace Finset

lemma inter_ne_empty_of_card_add_gt_card_univ (h : Fintype.card α < S.card + T.card) :
    (S ∩ T).Nonempty := inter_nonempty_of_card_lt_card_add_card S.subset_univ T.subset_univ h

[Christoph Spiegel]

Ah, so it was one of the pigeonhole statements after all, thanks!