Zulip Chat Archive

Stream: new members

Topic: basic Union


view this post on Zulip Pedro Castilho (Nov 10 2020 at 04:41):

hi am trying to complete the second lean sorry , but I don't really know what command I should use, I trying library search but didn't work.
it seem pretty straightforward getting y in union A form y in A i.

example : f '' ( i, A i) =  i, f '' A i :=
begin
unfold image,
dsimp,
ext1,
split,
dsimp,

{sorry},

intro h,
simp at h,
dsimp,
cases h with i h1,
cases h1 with y h2,
use y,
split,
have h3 : y  A i, from h2.1,
show y  Union A, from sorry

view this post on Zulip Alex J. Best (Nov 10 2020 at 04:55):

rw mem_Union

view this post on Zulip Alex J. Best (Nov 10 2020 at 04:56):

Should take it into the form that you can then feed in that y \in A i

view this post on Zulip Pedro Castilho (Nov 10 2020 at 04:59):

thx, it worked, but how could I have known that?

view this post on Zulip Pedro Castilho (Nov 10 2020 at 05:02):

now am trying a different problem in which I have x ∈ Inter A and am trying to reach x ∈ A I

view this post on Zulip Pedro Castilho (Nov 10 2020 at 05:04):

I tried to mimic your solution and gave a shot at rw mem_Inter

view this post on Zulip Pedro Castilho (Nov 10 2020 at 05:06):

oh, it did work when I applied it on the right place

view this post on Zulip Pedro Castilho (Nov 10 2020 at 05:06):

but still, how did you know what do next?

view this post on Zulip Alex J. Best (Nov 10 2020 at 05:15):

Pedro Castilho said:

thx, it worked, but how could I have known that?

with a little practice you can start guessing names of lemmas. You can also look in the file near where the term you are trying to get rid of is defined. if I click Union A in vscode a little box pops up with an arrow which takes me to the definition, and I see the lemma mem_Union a few lines below the definition. In fact in this case its a simp lemma, so simp would also make progress here.

view this post on Zulip Alex J. Best (Nov 10 2020 at 05:15):

Screen-Shot-2020-11-10-at-00.15.21.png

view this post on Zulip Alex J. Best (Nov 10 2020 at 05:16):

The \hookrightarrow arrow

view this post on Zulip Pedro Castilho (Nov 10 2020 at 14:27):

I actually tried clicking in the def of Union but it gave an error

view this post on Zulip Pedro Castilho (Nov 10 2020 at 14:28):

so I wasn't able to lookup this method

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 15:05):

Lean's maths library conforms to a pretty rigid naming convention, and VS Code provides a powerful interface to it. There's some #naming conventions which you might want to glance over.

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 15:19):

You used library_search too late @Pedro Castilho :-) Here's some proofs you might like :

import tactic

variables (I : Type) (X Y : Type) (f : X  Y) (A : I  set X)

open set -- so I don't have to keep writing set.blah

-- it's in the library
example : f '' ( i, A i) =  i, f '' A i :=
begin
  exact image_Union, -- I found this with `library_search`, but I could have guessed the name anyway
end

-- A powerful tactic can solve this by brute force
example : f '' ( i, A i) =  i, f '' A i :=
begin
  tidy
end

-- first principles proof -- click through it to see what's going on
example : f '' ( i, A i) =  i, f '' A i :=
begin
  ext y,
  split,
  { rintro x, hx, rfl⟩,
    rw mem_Union at *,
    cases hx with i hi,
    exact i, x, hi, rfl },
  { rw mem_Union,
    rintro i, x, hxi, rfl⟩,
    use x,
    rw mem_Union,
    exact ⟨⟨i, hxi⟩, rfl }
end

view this post on Zulip Pedro Castilho (Nov 11 2020 at 00:04):

uau, thank a lot @Kevin Buzzard , I didn't know about the names conventions that will really help

view this post on Zulip Pedro Castilho (Nov 11 2020 at 00:05):

and the proofs are great also

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 00:06):

A great trick with the names is to half-guess what the name might be, type that, and then press ctrl-space to see possible completions

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 00:30):

https://youtu.be/bghu6jVt0SY the second half of this shows the trick one can use


Last updated: May 09 2021 at 19:11 UTC