Nested congr in conv

Stream: general

[Floris van Doorn]

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]

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]

Oh, I did not know that. Thanks!

[Johan Commelin]

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]

I think the issue is more fundamental than goodies

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

right, I mean with combinators