Buggy `nth_rewrite`?

Stream: general

[Violeta Hernández]

The following proof breaks when the @ is removed, even though no arguments are actually specified.
https://github.com/leanprover-community/mathlib/blob/5eb68b5ca1cce3e5fd3cb3975e3af2b9d4f6149a/src/set_theory/ordinal/arithmetic.lean#L2210

[Violeta Hernández]

It gives a "no goals" error

[Mario Carneiro]

it isn't too surprising that something like that could happen; @foo is equivalent to foo _ _ so the first one allows rewrites with any applications of foo and the second one only allows rewrites with one particular (undetermined) set of arguments

[Violeta Hernández]

Weird

[Violeta Hernández]

So, this is normal/expected behavior?