Zulip Chat Archive

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