Fix terminology in L02rw.lean

[DecimalTurn]

This pull request includes a small change to the Game/Levels/Tutorial/L02rw.lean file. The change clarifies the language by replacing "proof" with "assumption" in the context of rewriting with the rw tactic.

[DecimalTurn]

After reading this another time, perhaps the best would just be to say "We do this in Lean by rewriting the proof, using the rw tactic.", since we are not rewriting h in this case, but the proof.

[kbuzzard]

Suggested change

	We do this in Lean by *rewriting* the proof with `h`,
	We do this in Lean by *rewriting* `h`,

How about that? Although I feel like I now want to change it back to "rewriting the assumption h".

The point is that the rw tactic eats a list of assumptions, and it rewrites them, so "rewriting the assumption h" sounds completely accurate to me.

[DecimalTurn]

@kbuzzard @joneugster thanks for both of your reviews. I see that we haven't come to a consensus yet. However, due to the way GitHub creates a separate thread for each review, I suggest that we discuss the wording in this main thread to make the discussion easier to follow.

From my understanding (and correct me if this is inaccurate), in Lean we start by stating a goal as a statement and transform this goal into a new statement each time we use a tactic. This then becomes our new current goal. We stop when we reach the statement "true" which indicates that we've accomplished our goal. The whole process, including all the intermediary goals, constitutes the proof.

Hence, when we use the rewrite tactic with the assumption h (ie. rw[h]), we are rewriting the current goal by "substituting in" all instances of the left-hand side of the assumption with the right-hand side. Based on that interpretation, the phrasing could be:

- We do this in Lean by *rewriting* the proof `h`, [...]
+ We do this in Lean by *rewriting* the goal with `h`, [...]

This wording makes it clear to me that we are rewriting the goal and not the entire proof nor h (since h is an assumption that which remains unchanged).

Let me know if this works and I'll make the change. I see that there is also some files in the .i18n that I haven't edited. I can also fix that.