mathlib3 documentation

tactic.nth_rewrite.basic

meta structure tactic.nth_rewrite.cfg  :

Configuration options for nth_rewrite.

A data structure to track rewrites of subexpressions. The field exp contains the new expression, while proof contains a proof that exp is equivalent to the expression that was rewritten.

Postprocess a tracked rewrite into a pair of a rewritten expression and a proof witness of the rewrite.