Commit 2025-03-12 23:13 241c1c00
View on Github →chore(Data/(E)(NN)Real): address porting notes (#22883) A lot of these porting notes are just plain TODOs, not regressions compared to Lean 3. There are a few remaining porting notes asking for reimplementation of tactic (positivity, norm_num) extensions.