## Stream: new members

### Topic: using union

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

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

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


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


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

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

#### Patrick Massot (Nov 07 2020 at 01:02):

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

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


#### Patrick Massot (Nov 07 2020 at 01:04):

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

#### Patrick Massot (Nov 07 2020 at 01:05):

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

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

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

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

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