Rewriting in proof assistants spans a strict hierarchy. Equational rewriting substitutes based on extensional equality; subequational rewriting substitutes based on homogeneous relations such as $\leq$ or $\subseteq$, justified by monotonicity lemmas; and generalized rewriting relates different operations across different types, justified by transfer rules. All three are specializations of one schema, the function relator $(R \Rightarrow S)\,f\,g$. Lean 4's rw and Mathlib's grw/gcongr implement the first two levels, but the third has had no Lean implementation. We present one: a transfer tactic family over a tagged rule database, benchmarked using Mathlib's own test suites, of which 112 of 178 ported tests close through the transfer engine. An evaluation of the design's three motivating hypotheses returns a mixed result: generality holds, authoring effort wins in its amortized form (averaged per use), but on dependency footprint, transfer only ties a mature library and loses on coercions. This shows that transfer's value is concentrated on transferring into domains where few theorems exist.

翻译：暂无翻译