Infinitary pigeonhole principle

Stream: new members

[Ching-Tsun Chou]

How do I prove the following formulation of the infinitary pigeonhole principle? I know I should use some result in ## Mathlib.SetTheory.Cardinal.Pigeonhole. But, alas, I don't know how to deal with statements involving aleph0 and ord.cof.

example (X : Type) [Finite X] (f : ℕ → X) (s : Set X)
  (h : ∃ᶠ k in atTop, f k ∈ s) : ∃ x ∈ s, {k | f k = x}.Infinite := by sorry

[Aaron Liu]

@loogle "exists", "infinite", "fiber"

[loogle]

:search: Cardinal.exists_infinite_fiber, Finite.exists_infinite_fiber

[Aaron Liu]

import Mathlib

open Filter

example (X : Type) [Finite X] (f : ℕ → X) (s : Set X)
    (h : ∃ᶠ k in atTop, f k ∈ s) : ∃ x ∈ s, {k | f k = x}.Infinite := by
  rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite] at h
  let uf := Set.restrictPreimage s f
  have : Infinite (f ⁻¹' s) := h.to_subtype
  obtain ⟨⟨x, hx⟩, hi⟩ := Finite.exists_infinite_fiber uf
  refine ⟨x, hx, ?_⟩
  rw [← Set.infinite_range_iff (Subtype.val_injective.comp Subtype.val_injective)] at hi
  conv =>
    enter [1, 1, k]
    equals f k ∈ s ∧ f k = x =>
      rw [eq_iff_iff, iff_and_self]
      rintro rfl
      exact hx
  simpa [Set.range_comp, Subtype.ext_iff, uf, Subtype.coe_image] using hi

[Ching-Tsun Chou]

Thanks for the pointer! I was not aware of Mathlib.Data.Fintype.Pigeonhole.