Commit 2025-01-10 18:19 ceb65893

chore: use ofNat more (#20546) When a theorem statement contains both ofNat and OfNat.ofNat, replace the latter by the former: as eric-wieser says, these are mostly theorems that work forwards, but not backwards, with simp. Very much not exhaustive, there are perhaps 160 instances in mathlib remaining.