## Stream: general

### Topic: Nested congr in conv

#### Floris van Doorn (Jan 05 2021 at 04:51):

Just posted lean#516. Reposting here for some visibility.

In the code snippet below, the second congr raises an error, presumably because I'm already "inside" an earlier congr. In my actual case I wanted to rewrite inside a double integral.

example : (∃ x y : ℕ, x = y) = true :=
begin
conv { to_lhs, congr, funext, congr, }
end


#### Alex J. Best (Jan 05 2021 at 04:55):

Probably you already know this but just in case a workaround in mathlib is to use nested conv:

example : (∃ x y : ℕ, x = y) = true :=
begin
conv { to_lhs, congr, funext, conv{ congr, funext,  } }
end


#### Floris van Doorn (Jan 05 2021 at 17:40):

Oh, I did not know that. Thanks!

#### Johan Commelin (Jan 05 2021 at 17:41):

we really need to "fix" conv mode. I think @Eric Wieser already added an exact tactic, but it wouldn't hurt to get some other common goodies.

#### Reid Barton (Jan 05 2021 at 17:43):

I think the issue is more fundamental than goodies

#### Reid Barton (Jan 05 2021 at 17:44):

I'm not sure you can actually navigate to all positions even

#### Eric Wieser (Jan 05 2021 at 17:45):

The exact tactic never made it through PR because I never bothered to add a test

#### Eric Wieser (Jan 05 2021 at 17:45):

I think you _can_ nagivate to all positions using docs#conv.interactive.find

#### Reid Barton (Jan 05 2021 at 17:46):

right, I mean with combinators

Last updated: May 15 2021 at 00:39 UTC