conv => ...
allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.
See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.
Basic forms:
-
conv => cs
will rewrite the goal with conv tacticscs
. -
conv at h => cs
will rewrite hypothesish
. -
conv in pat => cs
will rewrite the first subexpression matchingpat
(seepattern
).