## Stream: new members

### Topic: Using x ∈ z to convert y ∈ z to y = z

#### Eric Wieser (Jul 29 2020 at 17:03):

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 (Jul 29 2020 at 17:04):

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

#### Kevin Buzzard (Jul 29 2020 at 17:09):

convert hxz using 1

#### Eric Wieser (Jul 29 2020 at 17:10):

What is 1 there?

#### Kevin Buzzard (Jul 29 2020 at 17:10):

Where hxz is the proof that x is in z

#### Kevin Buzzard (Jul 29 2020 at 17:11):

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 (Jul 29 2020 at 17:11):

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 (Jul 29 2020 at 17:12):

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 (Jul 29 2020 at 17:12):

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

#### Mario Carneiro (Jul 29 2020 at 17:12):

How is this bug still not fixed?

#### Bryan Gin-ge Chen (Jul 29 2020 at 17:13):

Is there an open issue for it?

#### Mario Carneiro (Jul 29 2020 at 17:14):

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

#### Mario Carneiro (Jul 29 2020 at 17:14):

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

#### Mario Carneiro (Jul 29 2020 at 17:15):

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

#### Mario Carneiro (Jul 29 2020 at 17:16):

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

#### Mario Carneiro (Jul 29 2020 at 17:19):

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

#### Mario Carneiro (Jul 29 2020 at 17:20):

I guess we just need another case in parser_desc_aux

#### Mario Carneiro (Jul 29 2020 at 17:24):

lean#424

Last updated: Dec 20 2023 at 11:08 UTC