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 `StarOrderedRing`s, 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.

Archive/Imo/Imo1998Q2.lean

@@ -229,7 +229,7 @@ theorem clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
     (b - 1 : ℚ) / (2 * b) ≤ k / a ↔ ((b : ℕ) - 1) * a ≤ k * (2 * b) := by
   rw [div_le_div_iff]
   -- porting note: proof used to finish with `<;> norm_cast <;> simp [ha, hb]`
-  · convert @Nat.cast_le ℚ _ _ _ _
+  · convert Nat.cast_le (α := ℚ)
     · aesop
     · norm_cast
   all_goals simp [ha, hb]

Mathlib/Data/Nat/Cast/Basic.lean

@@ -84,30 +84,43 @@ theorem _root_.Commute.ofNat_right [NonAssocSemiring α] (x : α) (n : ℕ) [n.A
   n.commute_cast x
 
 section OrderedSemiring
+/- Note: even though the section indicates `OrderedSemiring`, which is the common use case,
+we use a generic collection of instances so that it applies in other settings (e.g., in a
+`StarOrderedRing`, or the `selfAdjoint` or `StarOrderedRing.positive` parts thereof). -/
 
-variable [OrderedSemiring α]
+variable [AddCommMonoidWithOne α] [PartialOrder α]
+variable [CovariantClass α α (· + ·) (· ≤ ·)] [ZeroLEOneClass α]
 
 @[mono]
 theorem mono_cast : Monotone (Nat.cast : ℕ → α) :=
   monotone_nat_of_le_succ fun n ↦ by
     rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one
 #align nat.mono_cast Nat.mono_cast
 
-@[simp]
-theorem cast_nonneg (n : ℕ) : 0 ≤ (n : α) :=
+@[simp low]
+theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
   @Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)
+
+-- without this more specific version Lean often chokes
+@[simp]
+theorem cast_nonneg {α} [OrderedSemiring α] (n : ℕ) : 0 ≤ (n : α) :=
+  cast_nonneg' n
 #align nat.cast_nonneg Nat.cast_nonneg
 
 section Nontrivial
 
-variable [Nontrivial α]
+variable [NeZero (1 : α)]
 
 theorem cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 :=
-  zero_lt_one.trans_le <| le_add_of_nonneg_left n.cast_nonneg
+  zero_lt_one.trans_le <| le_add_of_nonneg_left n.cast_nonneg'
 #align nat.cast_add_one_pos Nat.cast_add_one_pos
 
+@[simp low]
+theorem cast_pos' {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n <;> simp [cast_add_one_pos]
+
+-- without this more specific version Lean often chokes
 @[simp]
-theorem cast_pos {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n <;> simp [cast_add_one_pos]
+theorem cast_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} : (0 : α) < n ↔ 0 < n := cast_pos'
 #align nat.cast_pos Nat.cast_pos
 
 end Nontrivial