Commit 2026-09-22 11:41 4bbb1a27

chore: use simp instead of norm_num where simp suffices (#43035) This PR replaces norm_num with simp at 226 call sites where simp already closes the goal on its own. Most of these are (by norm_num) discharging a trivial side condition, for example pow_le_pow_of_le_one (by norm_num) (by norm_num), pow_pos (by norm_num) _, or logb_le_logb (b := 2) (by norm_num) _. norm_num runs the full default simp set and then dispatches its extensions on every subterm it visits, so where simp suffices the extension dispatch is pure overhead. The motivation is readability rather than speed. 🤖 Prepared with Claude Code