## Stream: general

### Topic: mem_preimage_eq

#### Patrick Massot (Jul 03 2019 at 13:59):

Is there any reason why mem_preimage_eq is stated as an equality rather than an iff? It seems contrary to the mathlib way

#### Chris Hughes (Jul 03 2019 at 14:02):

My guess is because it's stronger in the world without propext.

#### Kenny Lau (Jul 03 2019 at 14:04):

you can blame it on commit 8f4327a by digama0 on 15 Oct 2017:

#### Kenny Lau (Jul 03 2019 at 14:04):

or, in other words, it's because the code is 2 years old

#### Chris Hughes (Jul 03 2019 at 14:07):

I guess it means dsimp will use it.

Which is handy

@Mario Carneiro?

#### Mario Carneiro (Jul 03 2019 at 14:14):

I think it just predates the mathlib convention

#### Patrick Massot (Jul 03 2019 at 14:15):

Would you merge a PR changing this?

#### Mario Carneiro (Jul 03 2019 at 14:15):

also dsimp doesn't use iff.rfl lemmas unfortunately

#### Patrick Massot (Jul 03 2019 at 14:16):

Or maybe adding a mem_preimage_iff lemma if that dsimp thing is important?

#### Mario Carneiro (Jul 03 2019 at 14:16):

@Kenny Lau Actually that's not the origin; you can see it got moved in that commit but predates it

#### Mario Carneiro (Jul 03 2019 at 14:17):

I would merge such a PR

#### Mario Carneiro (Jul 03 2019 at 14:17):

I don't think the dsimp thing is a very big deal

#### Patrick Massot (Jul 03 2019 at 14:17):

Which version? Changing the lemma or adding a new one?

#### Mario Carneiro (Jul 03 2019 at 14:19):

changing the lemma

#### Patrick Massot (Jul 03 2019 at 14:22):

Should the new name be mem_preimage or mem_preimage_iff?

#### Mario Carneiro (Jul 03 2019 at 14:25):

I like mem_preimage if it's not already taken

#### Patrick Massot (Jul 03 2019 at 14:27):

It seems to exists in many namespaces but not the root one

#### Mario Carneiro (Jul 03 2019 at 14:27):

this one should be in the set namespace

actually it is

#### Patrick Massot (Jul 03 2019 at 14:28):

I didn't pay attention but this lemma is in the set namespace

#### Patrick Massot (Jul 03 2019 at 14:30):

Ok, let's see what Travis thinks about https://github.com/leanprover-community/mathlib/pull/1174

Last updated: May 13 2021 at 05:21 UTC