set.mem_image vs finset.mem_image

Stream: new members

[Antoine Chambert-Loir]

Here is the definition of docs#set.mem_image

 theorem set.mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y

and of docs#finset.mem_image

 theorem finset.mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {b : β} :
b ∈ finset.image f s ↔ ∃ (a : α) (H : a ∈ s), f a = b

Besides the specific notation '' for set images, you see that the right hand sides have different forms, which (it seems to me) makes the automatic translation from one to the other a bit awkward. (I noticed that while trying to pass a proof from sets to finsets.)
Should “one” wish to unify them ? and which form would be the preferred one?

[Eric Wieser]

I think we should definitely unify them to have the same form on the RHS

[Eric Wieser]

I'd lean towards the second one, since them simp can be used to take it into the first one if desired

[Eric Wieser]

But it doesn't matter much

[Antoine Chambert-Loir]

You mean that simp can create an and but tailord not to destruct it?
If I wish to do this unification, do I have to proceed as @Kevin Buzzard proposed me to do for commutators?

[Eric Wieser]

Simp knows about docs#exists_prop which rewrites the second lemma into the first

[Eric Wieser]

I'd wait for a second opinion on which is the better choice before embarking on the refactor

[Eric Wieser]

You could do a /poll

[Antoine Chambert-Loir]

In fact, I fell on this question while writing the following lemmas :

import tactic.basic
import data.finset.basic

variables {α : Type*} [decidable_eq α]

lemma test (a b: α) (f : α → α) (g : α → α) (hfg : function.left_inverse g f)
  (hb_fa : b = f a) : g b = a :=
begin
  change g b = id a,
  rw ← function.left_inverse.id hfg,
  apply congr_arg,
  exact hb_fa,
end

lemma test2 (f : α → α) (g : α → α) (hfg : function.left_inverse g f)
  (a : α) (s : finset α)
  (hb_fs : a ∈ finset.image f s) : g a ∈ s :=
begin
  obtain ⟨b, hb, rfl⟩ := finset.mem_image.mp hb_fs,
  change (g ∘ f) b ∈ s,
  rw function.left_inverse.id hfg,
  exact hb,
end

lemma test3 (f : α → α) (g : α → α) (hfg : function.right_inverse g f)
  (a : α) (s : finset α)
  (hb_fs : a ∉ finset.image f s) : g a ∉ s :=
begin
  by_contradiction hga_s,
  apply hb_fs,
  apply finset.mem_image.mpr,
  use g a,
  apply and.intro hga_s,
  change (f ∘ g) a = a,
  rw function.right_inverse.id hfg,
  refl,
end

Three more questions :

1) Should it exist explicitly in the library, as well as the analogues for sets.
(In the context of mul_action, f and g are actually an element of a group and its inverse, acting on a finset. For set, here is docs#mem_smul_set_iff_inv_smul_mem, but this is kind of the analogues for finset.)

2) Certainly you can do it quicker, using some existing suff (which I couldn't find)

3) If the two variants (for sets and finsets) have to coexist, should the proof of that for finsets reduce to the one for sets, using docs#finset.mem_coe or should they both be done directly ?

[Eric Wieser]

It might be worth editing the topic of that message so that the original question doesn't get lost

[Eric Wieser]

Those lemmas look like they might be related to docs#finset.preimage

[Antoine Chambert-Loir]

Eric Wieser said:

It might be worth editing the topic of that message so that the original question doesn't get lost

Do you have a suggestion? (In fact, I'm not sure of what you mean…)

[Eric Wieser]

You can edit a message and change its title.

[Johan Commelin]

I personally like ∃ x : α, x ∈ s ∧ f x = y better. It looks more like what one would write on paper.

[Yaël Dillies]

The advantage of the other proposition is that you only ever need to write ∃ x ∈ s, f x = y, which looks ever more like what you would write on paper.

[Antoine Chambert-Loir]

Eric Wieser said:

You can edit a message and change its title.

I found that but it is unclear what title you wish me to write. (I can change the title of what follows my second question, or change the title of the initial one…)

[Antoine Chambert-Loir]

I copy here links to a thread with answers of @Johan Commelin and @Yaël Dillies :
#new members > Questions about lemmas regarding images of sets/finsets