bad apply? suggestion

Stream: mathlib4

[Floris van Doorn]

The following snippet

import Mathlib.Tactic

example (n : ℕ) : True := by
  let N := n + 1
  have : N ≠ 1
  · apply?

gives as first suggestion

Try this: refine Ne.symm ((fun {M} [AddRightCancelMonoid M] {a b} ↦ self_ne_add_left.mpr) ?this.a)

which doesn't elaborate because of the fun-abstraction. This might of course just be a delaborator/pretty-printer issue.

Note that without the fun it does work:

refine Ne.symm (self_ne_add_left.mpr ?this.a)

Without using let we get completely different suggestions (and the first suggestion is actually way lower down).