# Zulip Chat Archive

## 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