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