using union

Stream: new members

[Pedro Castilho]

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?

[Bryan Gin-ge Chen]

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

[Pedro Castilho]

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

[Bryan Gin-ge Chen]

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

[Pedro Castilho]

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

[Pedro Castilho]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Pedro Castilho]

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

[Pedro Castilho]

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

[Bryan Gin-ge Chen]

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

[Pedro Castilho]

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