## Stream: new members

### Topic: Need help on proving {1,2,3} and P{1,2,3} are nontrivial

#### Lars Ericson (Dec 13 2020 at 01:08):

Proving that fin 3 is nontrivial works out of the box:

import data.finset.basic
example : nontrivial (fin 3) := fin.nontrivial


However, taking the powerset doesn't work: 𝒫 (fin 3)

So I need to change representations to

def X : set ℕ := ({1, 2, 3} : finset ℕ)


But then I'm not sure of a couple of things:

• How do I construct emptyset and top
• How do I use those constructed objects in a proof

I am stuck on that and sorry here:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
lemma is_nontrivial_X : ∃ (x y : X), x ≠ y := sorry


I have looked at library_search! which has no suggestions and output of suggest and hint which put out some ideas but haven't worked for me so far.

I'm also stuck for powerset. Here I've got 3 ideas and I don't know how to make them work:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
lemma empty_in_PX : (∅ ∈ (𝒫 X)) := sorry
lemma top_in_PX : (⊤ ∈ (𝒫 X)) := sorry
lemma is_nontrivial_PX : ∃ (x y : 𝒫 X), x ≠ y := sorry
instance : nontrivial (𝒫 X) := { exists_pair_ne := is_nontrivial_PX }


Any help greatly appreciated.

#### Yakov Pechersky (Dec 13 2020 at 01:17):

Why do you need that powerset?

#### Yakov Pechersky (Dec 13 2020 at 01:18):

The number of unique terms of "set (fin 3)" is the cardinality of that powerset

#### Alex J. Best (Dec 13 2020 at 02:29):

Nontrivial takes a type as input, not a set so it inserts a coercion which you may not want.
If all the elements you ever want to consider are 1,2,3 I'd recommend starting with fin 3 rather than making subsets of sets, you can just work with set (fin 3) more naturally in lean

def X : set ℕ := ({1, 2, 3} : finset ℕ)

lemma empty_mem_powerset : ∅ ∈ 𝒫 X := by simp
lemma top_in_PX : (⊤ ∈ (𝒫 X)) := sorry -- this is false ⊤ is the set of all naturals which is not a subset of X
lemma is_nontrivial_PX : ∃ (x ∈ 𝒫 X) (y ∈  𝒫 X), x ≠ y := ⟨ {1}, by simp [X], ∅, empty_mem_powerset, begin intros h, exact set.eq_empty_iff_forall_not_mem.mp h 1 rfl, end ⟩
instance : nontrivial (𝒫 X) := { exists_pair_ne := begin simp,rcases is_nontrivial_PX with ⟨x , hx, y, hy, h⟩, use [x, hx, y, hy],  end }


#### Lars Ericson (Dec 13 2020 at 02:32):

Thanks I will try set X . I got it in my head I needed 𝒫 X but that's incorrect.

#### Lars Ericson (Dec 13 2020 at 02:45):

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
refine nontrivial_of_ne _ _ _,
exact set.univ,
exact ∅ ,
exact set.empty_ne_univ.symm,
end


#### Eric Wieser (Dec 13 2020 at 08:21):

Does unfold X, apply_instance work for the second?

#### Lars Ericson (Dec 13 2020 at 14:36):

Yes

import data.finset.basic
def X := fin 3

instance : nontrivial (set X) :=
begin
unfold X,
apply_instance
end


#### Damiano Testa (Dec 14 2020 at 06:37):

Lars Ericson said:

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
refine nontrivial_of_ne _ _ _,
exact set.univ,
exact ∅ ,
exact set.empty_ne_univ.symm,
end


As far as I understand, the three exact after the refine fill in the underscores. Thus, also refine nontrivial_of_ne set.univ ∅ set.empty_ne_univ.symm, finishes the goal. At this point, you can notice that the last underscore is filled in with a proof that ∅ ≠ set.univ, so just this is enough for Lean to figure out what the two sets in question were. Hence, refine nontrivial_of_ne _ _ set.empty_ne_univ.symm,is sufficient information to create a proof. Once you are here, you no longer need tactic mode:

instance : nontrivial (set X) := nontrivial_of_ne _ _ set.empty_ne_univ.symm


Last updated: May 10 2021 at 00:31 UTC