mathlib documentation

tactic.transform_decl

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the function f. This is used to implement @[to_additive].

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the dictionary dict. This is used to implement @[to_additive].