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