patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
add
danabra.mov
+2
public/the-math-is-haunted/index.md
+2
public/the-math-is-haunted/index.md
···
174
174
175
175
The `rewrite` tactic is like a "find and replace" within your goal. If you have a proof that `a = b`, giving that proof to `rewrite` will rewrite your goal so that all `a` become `b` instead. Since `math_is_haunted` "proves" that `2 = 3`, `rewrite [math_is_haunted]` turned the goal from `⊢ 2 + 2 = 6` into `⊢ 3 + 3 = 6`.
176
176
177
+
(For the programmer-minded friends, this isn't some kind of string replacement. Some state-of-the-art pattern matching and type inference may be involved.)
178
+
177
179
And now that our goal is `⊢ 3 + 3 = 6`, our job is much easier. In fact, the `rfl` tactic alone will be enough to close *that* goal and thus complete the proof:
178
180
179
181
```lean {8}