Replace equals by equals
rw [h] substitutes using an equation, even inside functions no tactic can compute.
In this course 9 / 13
An equation you hold is a license to substitute. With h : a = b in the context, rw [h] replaces every a in the goal by b. This works anywhere inside the goal, including inside function applications that no tactic could compute, such as f a for an unknown function f.
After rewriting, rw tries rfl by itself. If the goal has become an equation whose two sides are identical, it closes on its own. Otherwise the rewritten goal stays open and you continue from it.
Several rewrites can go in one bracket: rw [h1, h2] rewrites with h1, then with h2. A proven equation from the library works the same way as a hypothesis. Nat.add_comm a b : a + b = b + a, so rw [Nat.add_comm] swaps the first sum it finds in the goal.
rw substitutes left to right: the left side of the equation must appear in the goal. If it does not, Lean says the motive or pattern was not found, which almost always means the equation points the other way or the expression is written differently.
Worked example
example (x y : Nat) (h : x = 3) (hy : y = 4) : x + y = 7 := by
rw [h, hy]After both rewrites the goal is 3 + 4 = 7, which rw closes by computation. In your exercise the goal is about an unknown function, so no computation helps and the rewrite has to set up an exact match with a hypothesis.
rw [h] substitutes using an equation, anywhere in the goal. It is the tool for goals that are equal by a fact rather than by computation.
Rewrite the goal with h so that it becomes exactly hb, then close it.
Suggested steps
- Replace
abybin the goal - Close the goal with the matching hypothesis
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct