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].
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].