Using `x ∈ z` to convert `y ∈ z` to `y = z`

Stream: new members

[Eric Wieser]

If I have x ∈ z as a hypothesis, and my goal is y ∈ z, is there an easy way to change the goal to x = y?

[Eric Wieser]

Preferably without having to actually spell out what x, y, and z are in my proof

[Kevin Buzzard]

convert hxz using 1

[Eric Wieser]

What is 1 there?

[Kevin Buzzard]

Where hxz is the proof that x is in z

[Kevin Buzzard]

You didn't say what x and y were, but if they are complex structures which are similar then convert might try to be too clever

[Alex J. Best]

1 says only to do 1 level of matching, so if x and y have other similarities it won't go too far

[Eric Wieser]

Looks like lean can't explain the syntax to me:

convert ← expr <error while executing interactive.param_desc: don't know how to pretty print lean.parser.small_nat>

[Eric Wieser]

Anyway, thanks for the speedy reply @Kevin Buzzard, that's exactly what I needed :)

[Mario Carneiro]

How is this bug still not fixed?

[Bryan Gin-ge Chen]

Is there an open issue for it?

[Mario Carneiro]

I thought there was a small_nat' parser in mathlib, but now I can't find it

[Mario Carneiro]

and of the search results it looks like more than half of small_nat uses are not guarded by with_desc

[Mario Carneiro]

although the actual description varies, it can be n or i or j

[Mario Carneiro]

I think we should just make small_nat in core have description n

[Mario Carneiro]

oh weird, src#interactive.param_desc is defined by recursion on expr instead of using typeclasses

[Mario Carneiro]

I guess we just need another case in parser_desc_aux

[Mario Carneiro]

lean#424