Commit 2026-01-09 10:48 2215f28e

fix(translate): don't unfold aux lemmas, but translate them (#33603) to_additive has some troublesome interactions with the module system, because it sometimes relies on unfolding theorems whose value is not exported. This PR fixes that by never unfolding these theorems, and instead creating their translation the first time they appear. This will help remove some instances of import all and instances of proofsInPublic. The only theorems that we still unfold are the auxiliary theorems created by simp. These have very small proofs, and these proofs are always exported, so it is fine to unfold them.