simp lemma for subtype.property

Stream: general

[Johan Commelin]

Should this be a simp lemma in mathlib?

import data.subtype

universe u

@[simp] lemma val_prop {X : Type u} {S : set X} (x : {x // x ∈ S}) : x.val ∈ S := x.property

[Mario Carneiro]

I'm not sure if it will work right as a simp lemma, but you are welcome to try

[Kenny Lau]

I would prefer this:

import data.set.basic

universe u

@[simp] lemma val_prop {X : Type u} {S : set X} (x : S) : ↑x ∈ S := x.property

[Mario Carneiro]

I'm guessing that the unfolding of x : S was performed by dsimp

[Mario Carneiro]

the simp lemma should be something that is in simp normal form already

[Kenny Lau]

only if you do dsimp *

[Kenny Lau]

how about we include both S and {x // x in S}

[Kenny Lau]

is x.val in simp normal form or \u x?

[Mario Carneiro]

I think they are both valid

[Kenny Lau]

so we have 4 versions!

[Mario Carneiro]

I don't think S vs {x // x in S} affects simp applicability

[Kenny Lau]

you're right

[Kenny Lau]

so 2 versions

[Johan Commelin]

I've succesfully applied the current version in the perfectoid project. I'll prepare a PR that adds both versions to data/subtype.