Commit 2025-08-20 02:52 3033a8cf

chore: deduplicate "transform at location" methods (#27562) Many metaprograms have the following general structure: the input is an expression e and the output is a new expression e', together with a proof that e = e'. Such a metaprogram produces a variety of tactics: it may be used to modify the goal, a specified hypothesis, or (via Tactic.Location) a combination of these. Roughly the same code for this is repeated throughout the library, for the tactics ring_nf, abel_nf, norm_num, push_neg and reduce_mod_char; possibly it originates from the ring_nf version, #552. This PR extracts this repeated code to stand-alone functions Mathlib.Util.AtLocation and Mathlib.Util.AtNondepPropLocation.