The Transfer aesop rule set — declaration module #
A rule set declared with declare_aesop_rule_sets is not visible in the file
that declares it (aesop's frontend only exposes it to importing files — the
reason Mathlib keeps each set in a tiny Init.lean). This module only
declares the set, so that Transfer/Integrations/AesopIntegration.lean (which imports it) can
register rules into it and invoke aesop (rule_sets := [Transfer]), and so the
named set is usable engine-wide by any downstream file.