2.23 Rewriting Strategies
Rewriting with equality is one of the most frequent operations in Lean. At scale, the challenge is not knowing that rw exists, but deciding what to rewrite, where, and in which direction so the proof remains stable and readable. Problem You have equalities available, but naive rewriting: fails because the shape does not match succeeds but makes the goal harder applies too broadly and breaks later steps You need a...