Commit 2025-12-19 12:06 03dd195d

chore: remove backward.privateInPublic from lakefile (#33034) This PR removes the global backward.privateInPublic true setting from the lakefile. It adds the setting locally to many declarations. This is technical debt that will need to be cleaned later. A few modules seem to be particularly problematic. In those the backward compatibility setting is enabled at the file level, instead of at the declaration level. Part of the diff has been created with the help of Claude. But it struggled to do things correctly at scale and speed. To help review, I'm giving some hints below on how to digest the diff. These might be useful in the future, so I suggest including them in the commit message.

Review hints

Deletions

This PR contains 14 deletions. They are contained in the following files:

$ git diff master --numstat | awk '$2 > 0 && $3 ~ /\.lean$/ {print $3}' | xargs git diff master --stat --
 Mathlib/Algebra/Lie/TraceForm.lean                | 4 ++--
 Mathlib/Analysis/SpecialFunctions/Exp.lean        | 4 +