synthesized type class instance is not definitionally equal

Stream: mathlib4

[Cody Roux]

I'm getting
synthesized type class instance is not definitionally equal to expression inferred by typing rules

in the following code:

...
have inst : Structure OmegaArith NatWithFiniteOmega := FinStruct T
rw [Formula.realize_rel]
...

more precisely:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  inst
inferred
  FinStruct T

My guess is that the have inst := ... is too opaque.

1. Is there an easy fix for this?
2. Am I probably doing things wrong that I have to manually create an instance?

For the latter the issue is that T is a local variable, and the class inference does not seem to want to apply FinStruct automatically.

I ask this in the Mathlib stream because I'm heavily relying on FirstOrder.Language, but please tell me if I should take this to the general chat.

[Wen Yang]

I don't know how to reproduce your problem. You'd better provide the #mwe .

[Kevin Buzzard]

Try changing have to let. have is extremely opaque -- it forgets the definition completely, it's only used for proofs not data.

[Cody Roux]

Ok that did it, thanks all.