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: Dec 20 2023 at 11:08 UTC