mathlib documentation

• to_rewrite_cfg : tactic.rewrite_cfg
• try_simp : bool
• discharger : tactic unit
• simplifier : expr → tactic (expr × expr)

Configuration options for nth_rewrite.

• exp : expr
• proof : tactic expr
• addr : option (list expr_lens.dir)

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.