# Zulip Chat Archive

## Stream: new members

### Topic: Coercions from finset to set

#### MinusGix (Nov 21 2022 at 17:36):

I'm trying to prove that the complement of each element of the set-of-sets `F`

is within `F`

. (This is for learning so that I can work up to more complicated proofs similar to it)

The confusion I'm having is on how to handle coercions, I don't feel like I have a good handle on manipulating those.

It seems like being able to tell Lean that `(↑{val := {0}, nodup := _})ᶜ ∈ F`

should be turned into a `{(0 : fin 3)}ᶜ ∈ F`

would simplify proving.

(Other comments on whether this is a bad way to be proving this would also be appreciated)

```
-- Minor question: is there a nicer way of writing something like this where it needs to use
-- some constant?
example :
∀ E ∈ ({∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ} : set (set (fin 3))),
Eᶜ ∈ ({∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ} : set (set (fin 3))) :=
begin
let F : set (set (fin 3)) := {∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ},
-- I have proofs for both of the below, but cutting them out for a smaller example
let compl0 : ({fin.of_nat' 0} : set (fin 3))ᶜ = ({fin.of_nat' 1, fin.of_nat' 2} : set (fin 3)), sorry,
let compl0_in : {fin.of_nat' 0}ᶜ ∈ F, sorry,
intros E Einp,
fin_cases E,
-- `∅ᶜ ∈ F`
-- This case is easy since it seems to turn it into a set automatically
{ sorry },
-- `(↑{val := {0}, nodup := _})ᶜ ∈ F`
{
convert compl0_in,
-- simp? is how I found this coe_eq_singleton theorem, but it would have been nicer to just have it be a set in the first place
simp only [finset.coe_eq_singleton], refl,
},
-- `(↑{val := {1}, nodup := _})ᶜ ∈ F`
{
exfalso,
-- use Einp to prove false, since `{1} ∉ F`
sorry,
},
-- todo, the rest of them
end
```

#### Kyle Miller (Nov 21 2022 at 17:46):

You can write that set you have by `({∅, {0}, {1, 2}, set.univ} : set (set (fin 3)))`

by the way

#### Kyle Miller (Nov 21 2022 at 17:50):

Regarding these `(↑{val := {0}, nodup := _})`

terms, I'm not sure exactly what's happening with `fin_cases`

here, but something seems like it's not working in an ideal way.

#### Kyle Miller (Nov 21 2022 at 18:38):

Here's how I might approach your statement:

```
import tactic.fin_cases
import tactic.norm_fin
def F : set (set (fin 3)) := {∅, {0}, {1, 2}, set.univ}
example : ∀ E ∈ F, Eᶜ ∈ F :=
begin
intro E,
simp [F],
rintro (rfl | rfl | rfl | rfl),
{ simp },
{ right, right, left, ext i, fin_cases i; norm_fin },
{ right, left, ext i, fin_cases i; norm_fin },
{ simp }
end
```

The tactic#rintro tactic is a way to do destructuring while doing `intro`

. When you give it `rfl`

then it will substitute the variable for you automatically.

#### Patrick Johnson (Nov 21 2022 at 18:46):

Nonterminal `simp [F]`

!

Last updated: Dec 20 2023 at 11:08 UTC