mathlib documentation

tactic.nth_rewrite.basic

meta structure tactic.nth_rewrite.cfg  :
Type

Configuration options for nth_rewrite.

meta structure tactic.nth_rewrite.tracked_rewrite  :
Type

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.