# Zulip Chat Archive

## Stream: maths

### Topic: Turn a set { y : Y | exists x \in A, y = f x } into (f '' A)

#### Ryan Lahfa (Apr 03 2020 at 14:15):

I often dabble with sets which are images or preimages but I'm not sure how to switch between those two forms easily, I often do quick proofs of what I mentioned in the title, which I feel sub-efficient.

I read many times the docs of sets but never found something close to those facts, I just realized that maybe it could be hidden in `set.range`

definition. But I'm not too much up-to-date with subtypes → sets relations.

#### Patrick Massot (Apr 03 2020 at 14:16):

MWE?

#### Johan Commelin (Apr 03 2020 at 14:17):

@Ryan Lahfa I think that you should almost always prefer the `f '' A`

form, and use `rw set.mem_image`

and friends when you have things like `x \in f '' A`

#### Ryan Lahfa (Apr 03 2020 at 14:18):

Let's take this small working example:

import tactic import data.real.basic import data.real.cau_seq import data.set import data.set.finite import data.finset import order.bounds import order.complete_lattice variable {X: Type} local attribute [instance] classical.prop_decidable -- on active la décidabilité partout. def suite_st_croissante [conditionally_complete_linear_order X] {S: set X} (Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) : ℕ → X := well_founded.fix nat.lt_wf (λ n suite_st_croissante, Inf (S \ { x : X | ∃ k < n, x = suite_st_croissante k H})) def suite_st_croissante_def [conditionally_complete_linear_order X] {S: set X} (Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ): suite_st_croissante Hinf Hset n = Inf (S \ { x: X | ∃ k < n, x = suite_st_croissante Hinf Hset k }) := well_founded.fix_eq _ _ _ def suite_st_croissante_nonempty [conditionally_complete_linear_order X] {S: set X} (Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ): (S \ { x: X | ∃ k < n, x = suite_st_croissante Hinf Hset k }).nonempty := begin set L := {x : X | ∃ (k : ℕ) (H : k < n), x = suite_st_croissante Hinf Hset k}, by_contra, apply Hinf, have a := set.not_nonempty_iff_eq_empty.1 a, have := set.diff_eq_empty.1 a, apply set.finite_subset, have HS_finite: ∀ y: ℕ, (({x : X | ∃ (k : ℕ) (H_1 : k < y), x = suite_st_croissante Hinf Hset k}).finite) := begin { intro y, -- this proof looks complicated for nothing. have: {x : X | ∃ (k : ℕ) (H_1 : k < y), x = suite_st_croissante Hinf Hset k} = (suite_st_croissante Hinf Hset) '' { i : ℕ | i < y} := begin ext, split, repeat { intro H1, simp at H1, simp, obtain ⟨ x, ⟨ hxy, heq ⟩ ⟩ := H1, use x, split, exact hxy, symmetry, exact heq, }, end, rw this, apply set.finite_image, apply set.finite_lt_nat, } end, exact HS_finite n, exact this, end

#### Ryan Lahfa (Apr 03 2020 at 14:19):

Johan Commelin said:

Ryan Lahfa I think that you should almost always prefer the

`f '' A`

form, and use`rw set.mem_image`

and friends when you have things like`x \in f '' A`

Okay, that was the answer I was converging by what I've seen, it is just that I feel like theorem statements look weird but I shouldn't think such things of statements… :D

#### Patrick Massot (Apr 03 2020 at 14:23):

Sorry, this is not minimal enough for me. It times out here.

#### Ryan Lahfa (Apr 03 2020 at 14:26):

I'll minimize it.

import data.real.basic import data.set variable {X: Type} local attribute [instance] classical.prop_decidable def suite_st_croissante [conditionally_complete_linear_order X] {S: set X} (Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) : ℕ → X := well_founded.fix nat.lt_wf (λ n suite_st_croissante, Inf (S \ { x : X | ∃ k < n, x = suite_st_croissante k H})) lemma suite_st_croissante_images [conditionally_complete_linear_order X] {S: set X} (Hinf: set.infinite S) (Hset: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)) (n: ℕ): {x : X | ∃ (k : ℕ) (H_1 : k < n), x = suite_st_croissante Hinf Hset k} = (suite_st_croissante Hinf Hset) '' { i : ℕ | i < n} := -- this proof looks complicated for nothing. begin ext, split, repeat { intro H1, simp at H1, simp, obtain ⟨ x, ⟨ hxy, heq ⟩ ⟩ := H1, use x, split, exact hxy, symmetry, exact heq, }, end

@Patrick Massot Is it better?

#### Mario Carneiro (Apr 03 2020 at 14:27):

your theorem (which should not be a `def`

) should be trivial by `simp`

#### Ryan Lahfa (Apr 03 2020 at 14:27):

Mario Carneiro said:

your theorem (which should not be a

`def`

) should be trivial by`simp`

Replacing the body by `by simp`

? I just tried it and it failed to simplify.

#### Mario Carneiro (Apr 03 2020 at 14:28):

maybe apply `ext`

first

#### Ryan Lahfa (Apr 03 2020 at 14:29):

Same, it just rewrite the (x \in A <=> x \in B) by (exists … <=> exists …)

#### Mario Carneiro (Apr 03 2020 at 14:30):

what?

#### Ryan Lahfa (Apr 03 2020 at 14:30):

It transforms the goal which is:

x ∈ {x : X | ∃ (k : ℕ) (H_1 : k < n), x = suite_st_croissante Hinf Hset k} ↔ x ∈ suite_st_croissante Hinf Hset '' {i : ℕ | i < n}

by

(∃ (k : ℕ), k < n ∧ x = suite_st_croissante Hinf Hset k) ↔ ∃ (x_1 : ℕ), x_1 < n ∧ suite_st_croissante Hinf Hset x_1 = x

#### Ryan Lahfa (Apr 03 2020 at 14:31):

which sounds finishable by `refl`

to me…

#### Mario Carneiro (Apr 03 2020 at 14:31):

note the equality is the wrong way around

#### Patrick Massot (Apr 03 2020 at 14:31):

`ext , simp [eq_comm]`

does it

#### Ryan Lahfa (Apr 03 2020 at 14:31):

Ah! Right

#### Patrick Massot (Apr 03 2020 at 14:31):

Yes, `eq_comm`

is the main ingredient here

#### Ryan Lahfa (Apr 03 2020 at 14:32):

@Patrick Massot Okay, so this happens because of this equality issue and `eq_comm`

is not a simp-lemma, should it be a simp-lemma though?

#### Mario Carneiro (Apr 03 2020 at 14:32):

no, this is fine

#### Mario Carneiro (Apr 03 2020 at 14:33):

`by ext; simp [eq_comm]`

is a fine proof

#### Mario Carneiro (Apr 03 2020 at 14:33):

still "trivial" in my book

#### Patrick Massot (Apr 03 2020 at 14:33):

Even better: rewrite the statement with the "correct" equality

#### Ryan Lahfa (Apr 03 2020 at 14:33):

Yes, agreed, that helped me a lot!

#### Kevin Buzzard (Apr 03 2020 at 15:05):

Ryan Lahfa said:

`eq_comm`

is not a simp-lemma, should it be a simp-lemma though?

It would loop, wouldn't it? I think the idea is to try and keep everything in the right order :-)

#### Mario Carneiro (Apr 03 2020 at 15:06):

No, it's specifically detected to be a symmetry lemma and does something with term orders to prevent it from looping. That's why `simp [eq_comm]`

works

#### Mario Carneiro (Apr 03 2020 at 15:07):

similar things happen with `simp [add_comm]`

or `simp [add_comm, add_assoc]`

#### Mario Carneiro (Apr 03 2020 at 15:08):

Probably if you had a more elaborate symmetry like lemma like `foo a b c = foo b c a`

then it would loop

#### Kevin Buzzard (Apr 03 2020 at 15:09):

I thought that if it was a job for add_comm and add_assoc you used something like `ac_refl`

. Are these really confluent enough for `simp`

? This is some inbuilt hack or something, right?

#### Mario Carneiro (Apr 03 2020 at 15:10):

Yes, I think `simp`

calls `ac_refl`

or the thing that drives it behind the scenes

Last updated: May 09 2021 at 10:11 UTC