# Zulip Chat Archive

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