extract a filtered-out element from a finset

Stream: new members

[Evan Lohn]

Hi, I proved a small fact about finsets and was wondering if there is a better/shorter way to do it. For any finset, if filtering with some predicate p removes some elements, then elements of p that do not satisfy p exist.

import data.finset.basic
import data.finset.card

lemma extract_filtered_element {α : Type*} {p: α → Prop} {s: finset α} [decidable_pred p] (h: finset.card (finset.filter p s) < finset.card s):
∃ x ∈ s, ¬ p x :=
begin
  nth_rewrite 1 ← finset.filter_card_add_filter_neg_card_eq_card p at h,
  nth_rewrite 0 ← add_zero (finset.filter p s).card at h,
  have := lt_of_add_lt_add_left h,
  rw finset.card_pos at this,
  cases this with x hx,
  use x,
  rw finset.mem_filter at hx,
  exact hx,
end

[Kevin Buzzard]

You could probably do the last four lines in one line using this.1 and pointy brackets

[Ruben Van de Velde]

Not with this.1, since this is an existential, but this works:

import data.finset.basic
import data.finset.card

lemma extract_filtered_element {α : Type*} {p: α → Prop} {s: finset α} [decidable_pred p] (h: finset.card (finset.filter p s) < finset.card s):
∃ x ∈ s, ¬ p x :=
begin
  nth_rewrite 1 ← finset.filter_card_add_filter_neg_card_eq_card p at h,
  nth_rewrite 0 ← add_zero (finset.filter p s).card at h,
  have := lt_of_add_lt_add_left h,
  rw [finset.card_pos, finset.nonempty] at this,
  exact exists_imp_exists (λ x hx, exists_prop.mpr (finset.mem_filter.mp hx)) this,
end

[Patrick Johnson]

You can also prove it using docs#finset.card_le_card_of_inj_on:

example {α : Type*} {p : α → Prop} {s : finset α}
  (h : (finset.filter p s).card < s.card) :
  ∃ x ∈ s, ¬p x :=
begin
  contrapose! h, exact finset.card_le_card_of_inj_on id
  (λa h₁, by rw finset.mem_filter; exact ⟨h₁, h _ h₁⟩) (by simp)
end

[Yakov Pechersky]

This lemma should be stated using docs#finset.nonempty

[Eric Wieser]

It should be an iff too, right?