[rw — Formalising Mathematics 0.1 documentation](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/rw.html) ## Summary The  `rewrite` and the `rw`tactics is are “substitute in” tactics. If `h : x = y` is a hypothesis then `rw [h]` changes all of the `x` s in the goal to `y` s. `rw` also works with iff statements: if `h : P ↔ Q` then `rw [h]` will replace all the `P` s in the goal with `Q` s. `rw` works up to syntactic equality, i.e. if `h : x = y` then `rw [h]` will only work if the goal contains something which is literally the same as `x`. A common mistake I see is people trying `rw [h]` when `h` is _not_ an equality, or an iff statement; most commonly people try it when `h` has type `P → Q`. This won’t work; you use the [apply](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/apply.html#tac-apply) tactic in this situation. ## Examples[](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/rw.html#examples "Link to this heading") 1. Faced with h : x = y ⊢ x ^ 2 = 1369 the tactic `rw [h]` will turn the goal into `y ^ 2 = 1369`. 2. `rw` works with `↔` statements as well. Faced with h : P ↔ Q ⊢ P ∧ R the tactic `rw [h]` will turn the goal into `⊢ Q ∧ R`. 3. `rw` can also be used to rewrite in hypotheses. For example given `h : x =y` and `h2 : x ^ 2 = 289`, the tactic `rw [h] at h2` will turn `h2` into `h2 :y ^ 2 = 289`. You can rewrite in multiple places at once – for example `rw[h] at h1 h2 h3` will change all occurrences of the left hand side of `h` into the right hand side, in all of `h1`, `h2` and `h3`. If you want to rewrite in a hypothesis and a goal at the same time, try `rw [h] at h1 ⊢` (type the turnstile `⊢` symbol with `\|-`). 4. `rw` doesn’t just eat hypotheses – the theorem `zero_add` says `∀ x, 0 + x= x`, so if you have a goal `⊢ 0 + t = 37` then `rw [zero_add]` will change it to `t = 37`. Note that `rw` is smart enough to fill in the value of `x` for you. 5. If you want to replace the right hand side of a hypothesis `h` with the left hand side, then `rw [← h]` will do it. Type `←` with `\l`, noting that `l` is a small letter `L` for left, and not a number `1`. 6. You can chain rewrites in one tactic. Equivalent to `rw [h1]`, `rw [h2]`, `rw[h3]` is `rw [h1, h2, h3]`. 7. `rw` will match on the first thing it finds. For example, `add_comm` is the theorem that `∀ x y, x + y = y + x`. If the goal is `⊢ a + b + c = 0` then `rw add_comm` will change it to `⊢ c + (a + b) = 0`, because if we strip away the notation then `a + b + c = add (add a b) c`, which gets changed to `add c (add a b)`. If you wanted to switch `a` and `b` then you can tell Lean to do this explicitly with `rw add_comm a b`. ## Further notes[](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/rw.html#further-notes "Link to this heading") 1. `rw` tries a weak version of `rfl` when it’s finished. Beginners can find this confusing; indeed I disabled this in the natural number game because users found it confusing. As an example, if your tactic state is h : P ↔ Q ⊢ P ∧ R ↔ Q ∧ R then `rw [h]` will close the goal, because after the rewrite the goal becomes `⊢Q ∧ R ↔ Q ∧ R` and `rfl` closes this goal. 1. A variant of `rw` is `rwa`, which is `rw` followed by the `assumption` tactic. For example if your tactic state is h1 : P ↔ Q h2 : Q ↔ R ⊢ P ↔ R then `rwa [h1]` closes the goal, because it turns the goal into `Q ↔ R` which is one of our assumptions. 2. If `h : x = y` and your goal is `⊢ x * 2 + z = x`, then `rw [h]` will turn _both_`x``s into ``y``s. If you only want to turn one of the ``x``s into a ``y`then you can use `nth_rw 1 [h]` (for the first one) or `nth_rw 2 [h]` (for the second one). 3. `rw` works up to [syntactic equality](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#syneq). This means that if `h : (P → False) ↔ Q`and the goal is `⊢ ¬P` then `rw [h]` will fail, even though `P → False` and `¬P` are definitionally equal. The left hand side has to match _on the nose_. 4. `rw` does not work under binders. Examples of binders are `∀` and `∃`. For example, if your goal is `⊢ ∀ (x : ℕ), x + 0 = 0 + x` then `rw [add_zero]`will not work. In situations like this you can either do `intro x` first, or you can use the more powerful `simp_rw` tactic; `simp_rw [add_zero]` works and changes the goal to `∀ (x : ℕ), x = 0 + x`.