fourth element

Stream: Is there code for X?

[Johan Commelin]

What is the best way of proving

lemma foo (n : ℕ) (a b c : Fin (n+4)) :
    ∃ d, ¬d = a ∧ ¬b = d ∧ ¬c = d := by
  sorry

[Yakov Pechersky]

Card univ sdiff {a, b, c} ge n + 4 - 3, so it is nonempty because + 1.

[Yakov Pechersky]

Then, once you get your x in univ sdiff {a, b, c}, simplify that hypothesis

[Yaël Dillies]

Something like (untested)

open Finset
lemma foo (n : ℕ) (a b c : Fin (n+4)) :
    ∃ d, ¬d = a ∧ ¬b = d ∧ ¬c = d := by
  by_contra! h
  replace h : Finset.univ ⊆ {a, b, c} := fun _ _ ↦ by simpa using h _
  aesop (add unsafe card_le_card) (add unsafe card_insert_le) (add unsafe le_trans)

[Yakov Pechersky]

import Mathlib

open Finset

lemma foo (n : ℕ) (a b c : Fin (n+4)) :
    ∃ d, ¬d = a ∧ ¬b = d ∧ ¬c = d := by
  have h3 : card {a, b, c} ≤ 3 := by
    refine (card_insert_le _ _).trans ?_; rw [Nat.succ_le_succ_iff]
    refine (card_insert_le _ _).trans ?_; rw [Nat.succ_le_succ_iff]
    simp [one_le_two]
  have : n + 1 ≤ card (univ \ {a, b, c}) := by
    rw [card_sdiff (by simp), card_fin, add_tsub_assoc_of_le (h3.trans _)]
    gcongr
    · rw [le_tsub_iff_le_tsub]
      · norm_num [h3]
      · norm_num [h3]
      · exact h3.trans (by norm_num)
    · norm_num
  obtain ⟨d, hd⟩ : (univ \ {a, b, c}).Nonempty := card_pos.mp (this.trans_lt' Nat.succ_pos')
  exact ⟨d, by simpa [not_or, eq_comm] using hd⟩

[Johan Commelin]

Thanks! With your hints I came up with

lemma exists_ne_ne_ne_of_four_le (n : ℕ) (hn : 4 ≤ n) (a b c : Fin n) :
    ∃ d, ¬a = d ∧ ¬b = d ∧ ¬c = d := by
  let S : Finset (Fin n) := {a, b, c}
  have hS : S.card ≤ 3 := by
    apply (card_insert_le _ _).trans
    apply Nat.succ_le_succ
    apply (card_insert_le _ _).trans
    apply Nat.succ_le_succ
    simp
  obtain ⟨d, hd⟩ : (Finset.univ \ S).Nonempty := by
    rw [← card_pos, card_sdiff (subset_univ _), card_fin, tsub_pos_iff_lt]
    apply lt_of_le_of_lt hS
    omega
  simp [not_or, @eq_comm _ d] at hd
  use d

[Eric Wieser]

I wonder if it's easier to say that there is an element not in Set.range f for f : α → β when card α < card β ?

[Johan Commelin]

Following the idea of @Yaël Dillies

open Finset in
lemma exists_ne_ne_ne_of_four_le (n : ℕ) (hn : 4 ≤ n) (a b c : Fin n) :
    ∃ d, ¬a = d ∧ ¬b = d ∧ ¬c = d := by
  by_contra! h
  replace h : Finset.univ ⊆ {a, b, c} :=
    fun d _ ↦ by simpa [or_iff_not_imp_left, eq_comm] using h d
  replace h := card_le_card h
  rw [card_fin] at h
  have : ¬ (4:ℕ) ≤ 3 := by decide
  apply this ((hn.trans h).trans _)
  apply (card_insert_le _ _).trans; apply Nat.succ_le_succ
  apply (card_insert_le _ _).trans; apply Nat.succ_le_succ
  simp

(since the aesop line didn't work)