## Stream: new members

### Topic: Universal over concrete finite set

#### Logan Murphy (Jul 16 2020 at 13:52):

Might be silly, but if one is trying to prove a predicate holds universally over a concrete, finite set, is there a way to enumerate the cases? E.g.

import data.nat.parity data.set.basic
open set nat

def s : set ℕ := {2, 4, 6, 8}

lemma silly : ∀ x ∈ s, even x :=
begin
intros x h,
-- case 1 : x = 2
-- case 2 : x = 4
-- etc.
end


#### Scott Morrison (Jul 16 2020 at 14:02):

If it is a finset then you can use fincases.

#### Scott Morrison (Jul 16 2020 at 14:07):

But there needs to be some evidence that your set is finite before this will be possible.

#### Kevin Buzzard (Jul 16 2020 at 21:16):

import data.nat.parity data.set.basic
open set nat

def s : set ℕ := {2, 4, 6, 8}

lemma silly : ∀ x ∈ s, even x :=
begin
rintros x h,
rcases h with rfl,
use 1, norm_num,
rcases h with rfl,
use 2, norm_num,
rcases h with rfl,
use 3, norm_num,
rw mem_singleton_iff at h, rw h,
use 4, norm_num
end


#### Alex J. Best (Jul 16 2020 at 21:21):

You could also use repeat like this:

def s : set ℕ := {2, 4, 6, 8}

lemma silly : ∀ x ∈ s, even x :=
begin
repeat {apply forall_insert_of_forall, swap, norm_num, },
simp,
end


Last updated: May 14 2021 at 23:14 UTC