How to perform selective rw on an expression in Lean?

Stream: new members

[Noah Stebbins]

Hey there! I'm Noah and I'm new to LEAN. I've been going through the Natural Number Game and have been loving it. One thing I came across is being unable to selectively apply the rw tactic where I match by an expression.

I'll give an example to show what I mean.

Screenshot-2024-06-02-at-1.14.06PM.png

In the screenshot above, I'd effectively like to perform rw [mul_comm b^d a] to flip the b^d and a but LEAN won't let me do this. Instead, I do nth_rewrite 3 [mul_comm]. Is there a way to apply tactics on expressions like b^d?

Thank you for taking the time to read this!

[Ruben Van de Velde]

Parentheses around b^d

[Noah Stebbins]

Thank you @Ruben Van de Velde ! That worked

[Ruben Van de Velde]

It's a pretty common issue :)

[Kevin Buzzard]

Is there a way of changing the way rw parses in NNG to make this issue go away?

[Kyle Miller]

An easy (but severe!) way would be to make the precedence for ^ higher than the precedence for function application. That would affect other things too though, like Nat.succ a^b would be the same as Nat.succ (a^b) rather than (Nat.succ a)^b.

[Kyle Miller]

It might be possible to make arguments to lemmas in rw parse at a different precedence level, but I'm afraid mul_comm b^d a might come out as mul_comm (b^(d a))