Commit 2026-08-21 16:38 a5d99846

fix(Translate): apply (attr := ...) attributes in order of application time (#42765) This PR sorts the (attr := ...) attributes in to_additive/to_dual so that they are applied in order of application time. This is consistent with the order in which attributes are applied by lean inside @[...] notation. This is important because simps needs to run after implicit_reducible.