elaborate eliminator

Stream: mathlib4

[Johan Commelin]

Is there a common fix for

failed to elaborate eliminator, expected type is not available

In this case the snippet is

instance DecidableEq [DecidableEq α] : DecidableEq (Multiset α)
  | s₁, s₂ => (Quotient.recOnSubsingleton₂ s₁ s₂) fun l₁ l₂ => decidable_of_iff' _ Quotient.eq

and the error is on Quotient.recOnSubsingleton₂ s₁ s₂.

[James Gallicchio]

That was the error I was seeing here but I have no idea if it's the same elaboration issue