# Zulip Chat Archive

## Stream: new members

### Topic: equality of sets

#### Logan Murphy (Sep 15 2020 at 19:58):

I feel like it should be trivial to prove (something like) the following equality, but I can't seem to do it with basic tactics and I can't seem to find anything in the library that helps. Any suggestions?

```
def S₁ : set ℕ := {1}
def S₂ : set ℕ := {3}
def fin_S : fin 2 → set ℕ := ![S₁, S₂]
def S : set ℕ := S₁ ∪ S₂
def sets_complete : (⋃ i : fin 2, fin_S i) = S :=
by sorry
```

#### Kevin Buzzard (Sep 15 2020 at 19:59):

Can you post an #mwe please? Your code doesn't work for me.

#### Chris B (Sep 15 2020 at 20:14):

edit: was not expecting that to be matrix.vec_cons

@Logan Murphy sets are defined as their membership predicate, so basic equality of sets stuff comes from functional and propositional extensionality (see `set.ext`

). You can find some of the definitions and lemmas in the documentation for `data.set`

:

https://leanprover-community.github.io/mathlib_docs/data/set/basic.html

#### Logan Murphy (Sep 15 2020 at 20:18):

Thank you Chris,

Sorry Kevin, forgot my transitive imports,

```
import data.matrix.notation
def S₁ : set ℕ := {1}
def S₂ : set ℕ := {3}
def fin_S : fin 2 → set ℕ := ![S₁, S₂]
def S : set ℕ := S₁ ∪ S₂
def sets_complete : (⋃ i : fin 2, fin_S i) = S :=
by sorry
```

#### Adam Topaz (Sep 15 2020 at 20:54):

This boils down to proving that every term of `fin 2`

is either `0`

or `1`

(also for arbitrary S_1, S_2). Is there a one-line proof of this?

```
import data.matrix.notation
def S₁ : set ℕ := {1}
def S₂ : set ℕ := {3}
def fin_S : fin 2 → set ℕ := ![S₁, S₂]
def S : set ℕ := S₁ ∪ S₂
lemma fin_2_eq (i : fin 2) : i = 0 ∨ i = 1 := sorry
def sets_complete : (⋃ i : fin 2, fin_S i) = S :=
begin
ext,
split,
{ rintro ⟨_,⟨i,rfl⟩,h⟩,
rcases fin_2_eq i with rfl|rfl,
left,
assumption,
right,
assumption },
{ rintro (h|h),
use S₁,
use 0,
refl,
assumption,
use S₂,
use 1,
refl,
assumption }
end
```

#### Adam Topaz (Sep 15 2020 at 20:57):

Maybe there is a much shorter proof for `sets_complete`

in your specific case where S_1 and S_2 are explicit singletons. I dont know.

#### Yakov Pechersky (Sep 15 2020 at 21:09):

```
lemma fin_2_eq (i : fin 2) : i = 0 ∨ i = 1 := by { fin_cases i; simp }
```

#### Adam Topaz (Sep 15 2020 at 21:09):

Ah, `fin_cases`

was the tactic I was missing :)

#### Kevin Buzzard (Sep 15 2020 at 21:19):

We were all missing it until Scott wrote it a few months ago

#### Kyle Miller (Sep 15 2020 at 21:52):

Yakov Pechersky said:

`lemma fin_2_eq (i : fin 2) : i = 0 ∨ i = 1 := by { fin_cases i; simp }`

I thought this was something the equation compiler could solve, but I guess not. There needed to be a third case with a proof of impossibility:

```
lemma fin_2_eq : Π (i : fin 2), i = 0 ∨ i = 1
| ⟨0, _⟩ := or.inl rfl
| ⟨1, _⟩ := or.inr rfl
| ⟨n+2, h⟩ := false.elim (by { cases h, cases h_a, cases h_a_a })
```

#### Kenny Lau (Sep 15 2020 at 21:55):

if you want good inductions, use `fin2`

#### Kevin Buzzard (Sep 15 2020 at 22:01):

Does `omega`

do the n+2 case?

#### Kyle Miller (Sep 15 2020 at 22:44):

Looks like `omega`

can't do it

#### Alex J. Best (Sep 15 2020 at 23:20):

`by simp [fin.ext_iff]; omega`

works, omega just needs a little help from simp.

#### Alex J. Best (Sep 15 2020 at 23:22):

Actually thats a bit of a red herring I guess.

```
by exfalso; revert h; omega
```

also works.

Last updated: May 14 2021 at 07:19 UTC