apply_fun: `internal exception: postpone`

Stream: mathlib4

[Eric Rodriguez]

I raised this as #9303, but I was told maybe it's best if I crosspost here. A mwe that triggers this:

import Mathlib.Tactic.ApplyFun

example (a b : Nat) (h : a = b) : False := by
  apply_fun ((·) + 1) at h

Now, I think the expression is nonsense (I'm not sure what ((·) + 1) does but from when I got some things to work I think it wanted a function) but I've never seen this failure mode.