Zulip Chat Archive

Stream: new members

Topic: using union


view this post on Zulip Pedro Castilho (Nov 07 2020 at 00:17):

hi am trying to prove f '' (⋃ i, A i) ⊆ ⋃ i, f '' A i, but am stuck with the ⋃ i, A I. this is how far I have gone

dsimp,
intro h,
cases h with y h₁,
have h₂: y  Union A, from h₁.1,
cases h₂ with i h₃,
have hf: f y = x, from h₁.2,
cases h₃ with w h₃,

Can some one give me a hint on how to continue?

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 00:21):

Hi Pedro, do you mind providing a full #mwe that we can copy and paste into our editors?

view this post on Zulip Pedro Castilho (Nov 07 2020 at 00:26):

sure, sorry

am trying to prove the following statement, but am not sure how to deal with ⋃ i, I know the following step in paper but can't figure it out in lean

section
open set function

variables {α β I : Type*}
variable  f : α  β
variable  A : I  set α

example : f '' ( i, A i)   i, f '' A i :=
begin
unfold image,
dsimp,
intro x,
intro h,
cases h with y h₁,
have h₂: y  Union A, from h₁.1,
cases h₂ with i h₃,
have hf: f y = x, from h₁.2,
cases h₃ with w h₄,

end

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 00:42):

This works:

import data.set

open set function

variables {α β I : Type*}
variable  f : α  β
variable  A : I  set α

example : f '' ( i, A i)   i, f '' A i :=
begin
  -- unfold image,
  -- dsimp,
  intros x h,
  cases h with y h₁,
  have h₂: y  Union A, from h₁.1,
  cases h₂ with i h₃,
  have hf: f y = x, from h₁.2,
  cases h₃ with w h₄,
  simp, -- `squeeze_simp` tells us that
        -- this uses the lemmas `mem_image` and `mem_Union`
  cases w with j hj, -- `i ∈ range A` is defeq to `∃ (y : I), A y = i`
        -- so we can apply `cases`
        -- (I'd normally use `rcases` or `obtain`,
        -- which are powered-up versions of `cases`)
  use [j,y],
  rw hj at h₄,
  split; assumption
end

view this post on Zulip Pedro Castilho (Nov 07 2020 at 00:52):

oh, thx @Bryan Gin-ge Chen , how would you use rcases and obtain? would it make the proof shorter?

view this post on Zulip Pedro Castilho (Nov 07 2020 at 00:59):

also, can you explain to me the last line? I remember seeing ; before but I forgot what it does

view this post on Zulip Patrick Massot (Nov 07 2020 at 01:02):

Semi-colon applies the next tactic to all goals generated by the previous one.

view this post on Zulip Patrick Massot (Nov 07 2020 at 01:03):

rintros, rcases and obtain allow to compress several steps at one by doing recursive cases, or intro and unpack at the same time, and also substitution at the same time. Something like:

example : f '' ( i, A i)   i, f '' A i :=
begin
  rintros x a, -, ⟨⟨i, rfl⟩, ha : a  A i⟩⟩, rfl⟩,
  exact f '' (A i), mem_range_self _, mem_image_of_mem f ha
end

view this post on Zulip Patrick Massot (Nov 07 2020 at 01:04):

Did you follow the tutorials project? Some of those tricks are explained there.

view this post on Zulip Patrick Massot (Nov 07 2020 at 01:05):

You can read tactics documentation at https://leanprover-community.github.io/mathlib_docs/tactics.html

view this post on Zulip Pedro Castilho (Nov 07 2020 at 01:10):

oh, i didnt use the tutorial, I was following online books, but am going to check it thanks

view this post on Zulip Pedro Castilho (Nov 07 2020 at 01:11):

but how come exact ⟨h₄, hf⟩ and split; assumption are both finishing the proof, I mean the first one is obvious but I can't quite get the second

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2020 at 01:19):

split; assumption applies tactic#split, which creates two goals, then it applies tactic#assumption to both of them.

view this post on Zulip Pedro Castilho (Nov 07 2020 at 01:21):

ah, that's right, thx for the help guys.


Last updated: May 17 2021 at 22:15 UTC