The rewrites tactic. #
rw? tries to find a lemma which can rewrite the goal.
rw? should not be left in proofs; it is a search tool, like apply?.
Suggestions are printed as rw [h] or rw [← h].
Equations
- One or more equations did not get rendered due to their size.