## Stream: general

### Topic: easy-in-maths union question

#### Kevin Buzzard (Apr 17 2018 at 13:07):

import data.set
universe u
example {X Y : Type u} (U : set X) (f : X → set Y) :
(⋃ (uu : {x // x ∈ U}), f uu.val) = ⋃₀(f '' U) := sorry


"Two ways of writing a union are the same".

#### Kevin Buzzard (Apr 17 2018 at 13:08):

This is a joy to prove in tactic mode using set.subset.antisymm

#### Kenny Lau (Apr 17 2018 at 13:08):

is "joy" sarcasm?

#### Kevin Buzzard (Apr 17 2018 at 13:08):

begin
apply set.subset.antisymm,
{ intros y Hy,
cases Hy with V HV,
cases HV with HV HyV,
cases HV with uu HuV,
change V = f (uu.val) at HuV,
existsi V,
existsi _,
exact HyV,
existsi uu.val,
exact ⟨uu.property,eq.symm HuV⟩
},
{ intros y Hy,
cases Hy with V HV,
cases HV with HV HyV,
cases HV with u HuV,
existsi V,
existsi _,
exact HyV,
existsi (⟨u,HuV.1⟩ : {x // x ∈ U}),
exact eq.symm HuV.2
}


no, not at all

#### Kevin Buzzard (Apr 17 2018 at 13:09):

I feel like goals like this are ones that I know I can crush

#### Kevin Buzzard (Apr 17 2018 at 13:09):

so it's a bit like grinding in the early Zeldas

#### Kevin Buzzard (Apr 17 2018 at 13:09):

you know you can do it and it's quite fun to do

#### Kevin Buzzard (Apr 17 2018 at 13:09):

But for something of this form which is trivially true in maths

#### Kevin Buzzard (Apr 17 2018 at 13:10):

my understanding is that one should seek a short "obfuscated" proof

#### Kevin Buzzard (Apr 17 2018 at 13:10):

i.e. pull a couple of things out the library and you're done

#### Kevin Buzzard (Apr 17 2018 at 13:10):

so I looked through data.set.lattice

and I found

#### Kevin Buzzard (Apr 17 2018 at 13:10):

open set
#check @sUnion_image
#check @Union_eq_sUnion_image
#check @sUnion_eq_Union
#check @set.sUnion_eq_Union'


#### Kevin Buzzard (Apr 17 2018 at 13:11):

all of which said "a union equals a union"

#### Kevin Buzzard (Apr 17 2018 at 13:11):

but I just can't put them all together

#### Kevin Buzzard (Apr 17 2018 at 13:11):

So I am wondering if this is a hole in the library or if I'm missing a trick

#### Kevin Buzzard (Apr 17 2018 at 13:11):

I don't know this file very well

#### Kenny Lau (Apr 17 2018 at 13:12):

example {X Y : Type u} (U : set X) (f : X → set Y) :
(⋃ (uu : {x // x ∈ U}), f uu.val) = ⋃₀(f '' U) :=


right

#### Kevin Buzzard (Apr 17 2018 at 13:19):

But this stinks because surely my strategy is basically the same

#### Kevin Buzzard (Apr 17 2018 at 13:19):

except I split the iff into two distinct implications

#### Kevin Buzzard (Apr 17 2018 at 13:19):

and then somehow simp failed to deal with either of them

#### Kenny Lau (Apr 17 2018 at 13:20):

simp simplifies iff's and equalities, lol

#### Kevin Buzzard (Apr 17 2018 at 13:20):

As I said, my simp-fu is weak

#### Kevin Buzzard (Apr 17 2018 at 13:20):

so that's the trick -- don't break the symmetry.

#### Kevin Buzzard (Apr 17 2018 at 13:20):

Thanks -- that was very instructive!

#### Kenny Lau (Apr 17 2018 at 13:21):

example {X Y : Type u} (U : set X) (f : X → set Y) :
(⋃ (uu : {x // x ∈ U}), f uu.val) = ⋃₀(f '' U) :=
set.ext \$ λ z, ⟨λ hz, by simpa using hz, λ hz, by simpa using hz⟩


#### Kenny Lau (Apr 17 2018 at 13:21):

splitting into two implications ^

#### Kevin Buzzard (Apr 17 2018 at 17:00):

so to prove X -> Y using simp, you intro h and then simpa using h?

right

#### Kevin Buzzard (Apr 17 2018 at 17:10):

This trick is sufficiently important that it should be mentioned in the simp docs.

Last updated: May 15 2021 at 00:39 UTC