## Stream: new members

### Topic: basic Union

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


#### Alex J. Best (Nov 10 2020 at 04:55):

rw mem_Union

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

#### Pedro Castilho (Nov 10 2020 at 04:59):

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

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

#### Pedro Castilho (Nov 10 2020 at 05:04):

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

#### Pedro Castilho (Nov 10 2020 at 05:06):

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

#### Pedro Castilho (Nov 10 2020 at 05:06):

but still, how did you know what do next?

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

#### Alex J. Best (Nov 10 2020 at 05:15):

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

#### Alex J. Best (Nov 10 2020 at 05:16):

The $\hookrightarrow$ arrow

#### Pedro Castilho (Nov 10 2020 at 14:27):

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

#### Pedro Castilho (Nov 10 2020 at 14:28):

so I wasn't able to lookup this method

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

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


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

#### Pedro Castilho (Nov 11 2020 at 00:05):

and the proofs are great also

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

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