Commit 2025-04-02 12:42 d3fb08bf

fix: have to_additive unfold aux lemmas before translation (#23559) This PR changes how to_additive approaches translation by first unfolding all aux lemmas. Unfolding aux lemmas was previously added in #14628, since it was observed that aux lemmas tend not to have enough context to properly be additivized. This was added as a step after processing any aux decls. The change here is to make the unfolding happen before processing aux decls. We now also abstract nested proofs in additivized definitions. Additionally, we use Meta.check instead of Meta.inferType to correctly check the type of the translated declaration. The aux lemma unfolding is necessary for the next Lean release (v4.19.0).