Kind of pigeonhole

Stream: Is there code for X?

[Antoine Chambert-Loir]

Here are 4 versions of basic pigeon hole principles that I need. Are there somewhere in mathlib?
(I have proofs, they are given below hidden by a spoiler.)

import Mathlib.Data.Set.Card

namespace Set

variable {α : Type*} {s t : Set α}

theorem ncard_pigeonhole [Finite α] (h : Nat.card α < s.ncard + t.ncard) :
  (s ∩ t).Nonempty := sorry

theorem ncard_pigeonhole_compl (h : s.ncard + t.ncard < Nat.card α) :
  (sᶜ ∩ tᶜ).Nonempty := sorry

theorem ncard_pigeonhole_compl'  (h : s.ncard + t.ncard < Nat.card α) :
  s ∪ t ≠ ⊤ := sorry

theorem ncard_pigeonhole' [Finite α]
  (h' : Nat.card α ≤ s.ncard + t.ncard) (h : s ∪ t ≠ ⊤) :
  (s ∩ t).Nonempty := sorry

[Antoine Chambert-Loir]

Proofs for the above results

import Mathlib.Data.Set.Card

namespace Set

variable {α : Type*} {s t : Set α}

theorem ncard_pigeonhole [Finite α]
    (h : Nat.card α < s.ncard + t.ncard) : (s ∩ t).Nonempty := by
  rw [← compl_ne_univ]
  intro h'
  apply not_le.mpr h
  rw [← ncard_union_add_ncard_inter]
  apply Nat.le_of_add_le_add_right
  rw [add_assoc, ncard_add_ncard_compl, h', ncard_univ, add_le_add_iff_right, ← ncard_univ]
  apply ncard_le_ncard (subset_univ _)

theorem ncard_pigeonhole_compl
    (h : s.ncard + t.ncard < Nat.card α) : (sᶜ ∩ tᶜ).Nonempty := by
  have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt h)
  apply ncard_pigeonhole
  apply Nat.lt_of_add_lt_add_left
  rw [← add_assoc, ncard_add_ncard_compl]
  simp only [Nat.card_eq_fintype_card, add_comm, add_lt_add_iff_left]
  apply Nat.lt_of_add_lt_add_left
  rw [ncard_add_ncard_compl, add_comm]
  exact h

theorem ncard_pigeonhole_compl'
    (h : s.ncard + t.ncard < Nat.card α) : s ∪ t ≠ ⊤ := by
  intro h'
  apply not_le.mpr h
  rw [← ncard_univ, ← top_eq_univ, ← h']
  exact ncard_union_le s t

theorem ncard_pigeonhole' [Finite α]
    (h' : Nat.card α ≤ s.ncard + t.ncard) (h : s ∪ t ≠ ⊤) : (s ∩ t).Nonempty := by
  rw [← ncard_pos]
  apply Nat.lt_of_add_lt_add_right
  rw [ncard_inter_add_ncard_union, zero_add]
  apply lt_of_lt_of_le _ h'
  rw [← not_le]
  intro H
  apply h
  rw [top_eq_univ, eq_univ_iff_ncard]
  apply le_antisymm _ H
  rw [← ncard_univ]
  exact ncard_le_ncard (subset_univ _)

[Kevin Buzzard]

(to quote code in spoiler blocks, use four backticks not three)

I am suspicious about the third one being a pigeonhole principle :-) The pigeonhole principle is that if you have two pigeons in one hole then there's one hole which contains two pigeons (or a mild generalization of this). In the third one you only have one pigeon and two holes.

[Antoine Chambert-Loir]

These are quantum pigeons. I have two boxes with pigeons, and some pigeon is in both boxes.

[Ruben Van de Velde]

It's dual waves hands

[Antoine Chambert-Loir]

(This said, it is remarkable that the stuff I do in mathlib always ends up in proving stuff like that, which is never difficult, but neither direct. These results wouldn't even been proved in research papers!)

[Kevin Buzzard]

What they told us in 2017 was that if we kept doing nontrivial projects then we would quickly ensure that all the API for basic stuff was complete and after a while we'd never have to prove a basic theorem ever again. I am beginning to wonder whether this is true!

[Ruben Van de Velde]

I think ncard didn't exist in 2017

[Antoine Chambert-Loir]

The stuff would work with docs#Finset.card. (By the way, if such a thing goes into mathlib, under what form should it?)

[Kevin Buzzard]

There are apparently 20 pigeonhole principles in Mathlib/Combinatorics/Pigeonhole.lean so by the pigeonhole principle you would imagine that your theorems are there somewhere, but it seems that all of them involve finite sums rather than just two sets.

[Kevin Buzzard]

We need a good upper bound for the number of pigeonhole principles

[Antoine Chambert-Loir]

It's forbidden to feed the pigeons.

[Kevin Buzzard]

Maybe docs#Set.exists_ne_map_eq_of_ncard_lt_of_maps_to is the only tool which we have for two sets right now.

[Kevin Buzzard]

(oh let me revise my spoiler comment: to quote code in spoiler blocks you apparently need to write ````lean to get syntax highlighting)

[Antoine Chambert-Loir]

This is that lemma, applied to the map from the Sigma type of my two sets to the ambient set. This will take longer to translate than the actual proof!

[Jz Pan]

Kevin Buzzard said:

What they told us in 2017 was that if we kept doing nontrivial projects then we would quickly ensure that all the API for basic stuff was complete and after a while we'd never have to prove a basic theorem ever again. I am beginning to wonder whether this is true!

I think we should expect that all these basic stuff should be proven by AI tools so we don't need to prove them by ourselves. Is this happening?

[Antoine Chambert-Loir]

If such a thing is to happen, then I'll leave the field.

[Martin Dvořák]

I would like to have all of the above in Mathlib.
BTW, I recently PRed a few more pidgeonholes:
#22792

[Yaël Dillies]

Careful to PR more pigeons simultaneously!

[Yaël Dillies]

Antoine Chambert-Loir said:

If such a thing is to happen, then I'll leave the field.

Out of interest, why is that so?

[Antoine Chambert-Loir]

Because AI, by which I mean the thing which is presently developed by means of tremendous amounts of money and energy, is a threat to humanity.

[Bhavik Mehta]

There's docs#Finset.inter_nonempty_of_card_lt_card_add_card, which is the closest thing I'm aware of to what you're looking for. Putting variants of this for Finset into the Pigeonhole.lean file, plus a duplicate of that file for Set.ncard, seems reasonable to me. All of these should have short proofs, but it's useful to have them all in one place (and explicitly written in mathlib) so that someone unfamiliar with cardinality in mathlib (whether it be Finset.card or Set.ncard) can easily find what they need.