Using pigeonhole principle

Stream: new members

[Sabbir Rahman]

I am trying to understand how to use pigeonhole principle in general, searching in leansearch I got bunch of results. But I'm still not sure how to use them. For example, consider the most basic example, proving that among n + 1 numbers there exist at least two which have same remainder modulo n, how would I prove that? In fact the statement itself can be formalized in several ways, which is the best formalization to start with if I want to use pigeonhole

[Ruben Van de Velde]

Please share the formalizations of the statement you have tried

[suhr]

1. Decide ∀i j, i ≥ n+1 ∨ j ≥ n+1 ∨ i%n = j%n → i = j
2. If you found a counterexample, congrads
3. If not, then you have that % n is injective on {i // i < n+1}. Lead it to contradiction.

[Sabbir Rahman]

for my purposes, I had following statement

import Mathlib

example (n : ℕ) (hn : 0 < n) (s : Set ℕ) (hs : n < s.encard) :
    ∃ a ∈ s, ∃ b ∈ s, a ≠ b ∧ (a : ZMod n) = b := by
  sorry

I thought about using the fact that ZMod.card, but didn't really understand how to use that. I guess ZMod is not suitable to use for pigeonhole principle?

[Philippe Duchon]

Searching for "pigeonhole" in Mathlib seems to mainly find things for infinite pigeonhole, so my guess is, you should be looking for lemmas about cardinals and injectivity - since your statement is essentially that the function "modulo n" function is not injective on your set s.

That being said, there seems to be several versions of the notion of a cardinality in the library, so you might have to also navigate between them.

[Kyle Miller]

import Mathlib

example (n : ℕ) (hn : 0 < n) (s : Set ℕ) (hs : n < s.encard) :
    ∃ a ∈ s, ∃ b ∈ s, a ≠ b ∧ (a : ZMod n) = b := by
  have : NeZero n := NeZero.of_pos hn
  let f : s → ZMod n := fun x => x
  obtain _ | _ := finite_or_infinite s
  · have := Fintype.ofFinite s
    have : Fintype.card (ZMod n) < Fintype.card s := by
      rw [ZMod.card]
      rw [Set.encard_eq_coe_toFinset_card, Set.toFinset_card] at hs
      norm_cast at hs
    obtain ⟨⟨a,ha⟩, ⟨b, hb⟩, h1, h2⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
    use a, ha, b, hb, ?_, h2
    simpa using h1
  · obtain ⟨⟨a,ha⟩, ⟨b, hb⟩, h1, h2⟩ := Finite.exists_ne_map_eq_of_infinite f
    use a, ha, b, hb, ?_, h2
    simpa using h1

[Kyle Miller]

I might be missing the encard version of an "exists_ne_map_eq_of_*" theorem, but here's a way to get it done using a case split.