porting autoparams with identifiers

Stream: mathlib4

[Thomas Murrills]

What should be done about the occasional invalid auto tactic, identifier is not allowed situations (where an identifier is used in an autoparam)? (This occurs in e.g. Data.List.Basic.)

Take away the autoparams and leave a porting note? Or is there a workaround?