Commit 2023-07-31 14:06 a4f25598

feat: generalize a few Nat.cast lemmas (#6229) This generalizes some Nat.cast lemmas from OrderedSemiring α to the conjunction of AddCommMonoidWithOne α, PartialOrder α, CovariantClass α α (· + ·) (· ≤ ·), ZeroLEOneClass α; collectively, these make up an OrderedAddCommMonoidWithOne, but that type class doesn't actually exist. This generalization is not without purpose, the new lemmas will apply to StarOrderedRings, as well as the selfAdjoint part thereof, as well as the subtype {x : α // 0 ≤ x} of positive elements in a StarOrderedRing. These can be seen in #4871. Because we are generalizing some fundamental simp lemmas from a single bundled type class to a bag of several classes, Lean had trouble in a few places. So, we opt to keep the OrderedSemiring versions of these simp lemmas as a special case, and we mark the more general versions with @[simp low]. This also avoids needing to update the positivity extension for Nat.cast to the more general setting for the time being.