How do I prove this painfully obvious statement?

Stream: Is there code for X?

[Ching-Tsun Chou]

Alas, I have trouble proving the following painfully obvious statement. I'd appreciate any ideas.

example {X : Type*} [Finite X] (f : Fin (Nat.card X + 2) → Option X)
    (h : {j | (f j).isSome}.ncard = Nat.card X + 1) :
    ∃ j1 j2, j1 ≠ j2 ∧ ∃ x, f j1 = some x ∧ f j2 = some x := by
  sorry

The size of the Fin type can be any natural number ≥ Nat.card X + 1. It just happens to be Nat.card X + 2 in my particular use case.

[Aaron Liu]

@loogle Exists, Nat.card, Ne, Eq, LT.lt

[loogle]

:shrug: nothing found

[Aaron Liu]

well I guess you can always use the Fintype version docs#Fintype.exists_ne_map_eq_of_card_lt

[Kyle Miller]

The argument is that if you restrict to the given domain then it's the pigeonhole principle. The theorem Aaron cites works well enough for that.

Most of the complication is rephrasing the goal to use this restricted function.

import Mathlib

example {X : Type*} [Finite X] (f : Fin (Nat.card X + 2) → Option X)
    (h : {j | (f j).isSome}.ncard = Nat.card X + 1) :
    ∃ j1 j2, j1 ≠ j2 ∧ ∃ x, f j1 = some x ∧ f j2 = some x := by
  have := Fintype.ofFinite X
  let f' : { j | (f j).isSome} → X := fun j => (f j).get j.property
  have := Fintype.exists_ne_map_eq_of_card_lt f' ?card
  case card =>
    simp_rw [Set.ncard_eq_toFinset_card', Set.toFinset_setOf, Nat.card_eq_fintype_card] at h
    simp [Fintype.card_subtype, h]
  obtain ⟨x, y, hxy, h⟩ := this
  use x, y
  constructor
  · rwa [Subtype.coe_ne_coe]
  use f' x
  constructor
  · simp [f']
  · rw [h]
    simp [f']

I'm sure somewhere there are some other useful variants that could simplify this.

[Ching-Tsun Chou]

Following a pointer from the pigeonhole principle that Aaron pointed out, I ended up with the following proofs:

import Mathlib
open Function Set Prod Option Filter

example {X : Type*} [Finite X] (f : Fin (Nat.card X + 2) → Option X)
    (h : {j | (f j).isSome}.ncard = Nat.card X + 1) :
    ∃ j1 j2, j1 ≠ j2 ∧ ∃ x, f j1 = some x ∧ f j2 = some x := by
  have ht : (some '' (univ : Set X)).Finite := by exact toFinite (some '' univ)
  have : (some '' (univ : Set X)).ncard = Nat.card X := by
    rw [ncard_image_of_injective (univ : Set X) (some_injective X)]
    exact ncard_univ X
  have hc : (some '' (univ : Set X)).ncard < {j | (f j).isSome}.ncard := by omega
  have hf : ∀ j ∈ {j | (f j).isSome}, f j ∈ some '' (univ : Set X) := by
    intro j ; simp ; rw [isSome_iff_exists] ; tauto
  obtain ⟨j1, h_j1, j2, h_j2, h_ne, h_eq⟩ := exists_ne_map_eq_of_ncard_lt_of_maps_to hc hf ht
  obtain ⟨s1, h_s1⟩ := isSome_iff_exists.mp h_j1
  obtain ⟨s2, h_s2⟩ := isSome_iff_exists.mp h_j2
  simp [h_s1, h_s2] at h_eq ; obtain ⟨rfl⟩ := h_eq
  use j1, j2 ; simp [h_ne] ; use s1