at introduced without explanation

[sullyj3]

This is a great resource, thanks!

In implication world level 2/11

Objects:
yx: ℕ
Assumptions:
h: 0 + x = 0 + y + 2
Goal:
x = y + 2

the hint says "Rewrite zero_add at h twice, to change h into the goal."
At that point I hadn't yet encountered the concept of rewriting an assumption as opposed rewriting to the goal yet, so I didn't understand what was being asked of me. I eventually figured out the syntax was just rewrite [zero_add] at h with the help of chatgpt.

[joneugster]

Thanks for reporting, and sorry we only fixed the wording now.

[StevenClontz]

Fun fact, @Not-Abram and I just today encountered this issue and were going to make a pull request to address it. My guess is that there's a build process that hasn't run to update the live site yet.

However, our thought was that rather than explicitly suggesting the full rw [zero_add] at h snippet in the commentary, this might be a good opportunity to suggest to players to look at the built-in documentation for rw. Something like:

We can use the rw tactic to change not just a goal, but also to change our hypotheses. To learn how to rewrite at a hypothesis, check the summary for rw by clicking it in the right sidebar. Two rewrites of zero_add at h should do the trick here.

If that sounds like an enhancement, I'll get @Not-Abram to make the PR.