# Zulip Chat Archive

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

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

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`

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

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) := set.ext $ λ z, ⟨λ ⟨x1, ⟨⟨x2, H1⟩, H2⟩, H3⟩, ⟨x1, ⟨x2, H1, H2.symm⟩, H3⟩, λ ⟨x1, ⟨x2, H1, H2⟩, H3⟩, ⟨x1, ⟨⟨x2, H1⟩, H2.symm⟩, H3⟩⟩

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

I need to be quick because my daughter just woke up (she is sick and off school)

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

but while I'm here let me mention the independent question that I was talking about `existsi _`

yesterday or so and Mario advised me not to use it, saying it was better to go back and fill it in later.

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

However in my proof above, I used it because the thing that exists is another existsi

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

Aah excellent -- that looks much more like the 2-line obfuscated proof which this result deserves.

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

Should it be in the library?

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

Thanks Kenny.

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

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

#### Johannes Hölzl (Apr 17 2018 at 13:15):

the simplifier also works: `by simp [set.set_eq_def]`

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

now we just switched camps :P

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

Aah! I tried to use simp a lot too, but my simp-fu is weak.

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

Thanks Johannes. How long did it take you to find that?

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

You see, the long tactic mode proof took me a very short time to write, because at each stage I just did the only thing which could be done.

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

I suspect that Kenny had a similar experience with the term proof.

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

But when I tried to find a short proof using library functions, all that happened was that I spent a long time looking through the library and noting down possibly useful functions

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

and then a long time failing to glue them together.

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

I want to get to the stage where if it's easy in maths, I can just nail it in Lean

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

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

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

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`

?

#### Kenny Lau (Apr 17 2018 at 17:03):

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