Weird conv bug

Stream: lean4

[Yongyi Chen]

import Mathlib

example : Fintype.card {x // x = 3} = Fintype.card {x // x = 3} := by
  conv in _ = 3 =>
    skip

Output: [error when printing message: unknown goal _uniq.75345]

Goes away if I replace Fintype with Nat.

[Tomas Skrivan]

I have encountered something similar previously and it seems that the conv tactic pattern _ is buggy. Yours conv in ... is just a syntax sugar for calling pattern _.

[Kyle Miller]

Are you able to navigate to x = 3 using other conv tactics? The Fintype.card function is especially tricky since it has an instance argument that depends on the first argument. One reason we have Nat.card in mathlib is to avoid this complexity.

[Yongyi Chen]

No, I could not find a way to navigate to x = 3.