an error maybe comes from local notation

Stream: new members

[Z. X. Wang]

Have you ever met such error when use apply?:
found a proof, but the corresponding tactic failed: (expose_names; exact abs_sum_le_sum_abs (fun i_1 ↦ algJ.M i i_1 * y i_1) {t | t ≥ i})

The above message is not colored and cannot be clicked to apply directly.
but i can copy this message, then replacing the algJ.M with (Jacobi A hA b x0).M, to finish my proof. The algJ.M is a local notation of (Jacobi A hA b x0).M, that is:

local notation "algJ.M" => (Jacobi A hA b x0).M

[Ruben Van de Velde]

I've seen that, yeah, and usually the proof does still work with some adjustment

[Z. X. Wang]

i want to know the reason. And can we improve the tactic apply? to solve this problem?

[Kyle Miller]

It looks like it could be the fact that binding domains aren't being pretty printed. Maybe try set_option pp.funBinderTypes true and see if that improves things?