Delaborator for "not an element" doesn't check for mdata

The delaborator delab_not_in (in Mathlib/Utli/Delaborators.lean) doesn't check for mdata, and as a result it gives the wrong result in certain situations. These examples illustrate the problem:

import Mathlib.Tactic

example (A : Set Nat) : 0 ∈ A := by
  by_contra h

example (A : Set Nat) : 0 ∈ A := by
  have h1 : 0 = 0 := by rfl
  by_contra h

In the first example, after the by_contra tactic, the display of h in the tactic state is h : 0 ∉ A. But in the second example, it is h : ¬0 ∈ A. The reason for the difference is that in the second example, the type of h has the form:

(app (const Not []) (mdata [(noImplicitLambda, true)] (app (app (app (app (app (const Membership.mem ...

It is the presence of the mdata that causes the delaborator to fail to recognize this as the negation of a membership statement. In the first example, the mdata isn't there, and the delaborator works correctly.

It seems like adding a call to consumeMData should fix the problem.

Open Mathlib/Utli/Delaborators.lean and inspect delab_not_in, then reproduce the two by_contra examples from the issue to compare their tactic-state output. Check how mdata is handled around membership negation; done means both examples display h as 0 ∉ A.