chore(*): generalize some lemmas from linear_ordered_semiring to `o…

…rdered_semiring` (#5327)

API changes:

* Many lemmas now have weaker typeclass assumptions. Sometimes this means that `@myname _ _ _` needs one more `_`.
* Drop `eq_one_of_mul_self_left_cancel` etc in favor of the new `mul_eq_left_iff` etc.
* A few new lemmas that state `monotone` or `strict_mono_incr_on`.

archive/imo/imo1998_q2.lean

@@ -194,12 +194,7 @@ local notation x `/` y := (x : ℚ) / y
 
 lemma clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
   (b - 1) / (2 * b) ≤ k / a ↔ (b - 1) * a ≤ k * (2 * b) :=
-begin
-  rw div_le_div_iff,
-  { convert nat.cast_le; finish, },
-  { simp only [hb, zero_lt_mul_right, zero_lt_bit0, nat.cast_pos, zero_lt_one], },
-  { simp only [ha, nat.cast_pos], },
-end
+by rw div_le_div_iff; norm_cast; simp [ha, hb]
 
 theorem imo1998_q2 [fintype J] [fintype C]
   (a b k : ℕ) (hC : fintype.card C = a) (hJ : fintype.card J = b) (ha : 0 < a) (hb : odd b)

src/algebra/archimedean.lean

@@ -46,18 +46,21 @@ end
 
 end linear_ordered_add_comm_group
 
-theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
+theorem exists_nat_gt [ordered_semiring α] [nontrivial α] [archimedean α]
   (x : α) : ∃ n : ℕ, x < n :=
 let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
 ⟨n+1, lt_of_le_of_lt (by rwa ← nsmul_one)
   (nat.cast_lt.2 (nat.lt_succ_self _))⟩
 
-theorem exists_nat_ge [linear_ordered_semiring α] [archimedean α] (x : α) :
+theorem exists_nat_ge [ordered_semiring α] [archimedean α] (x : α) :
   ∃ n : ℕ, x ≤ n :=
-(exists_nat_gt x).imp $ λ n, le_of_lt
+begin
+  nontriviality α,
+  exact (exists_nat_gt x).imp (λ n, le_of_lt)
+end
 
-lemma add_one_pow_unbounded_of_pos [linear_ordered_semiring α] [archimedean α] (x : α) {y : α}
-  (hy : 0 < y) :
+lemma add_one_pow_unbounded_of_pos [ordered_semiring α] [nontrivial α] [archimedean α]
+  (x : α) {y : α} (hy : 0 < y) :
   ∃ n : ℕ, x < (y + 1) ^ n :=
 let ⟨n, h⟩ := archimedean.arch x hy in
 ⟨n, calc x ≤ n •ℕ y : h
@@ -208,7 +211,7 @@ variables [linear_ordered_field α]
 
 theorem archimedean_iff_nat_lt :
   archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
-⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
+⟨@exists_nat_gt α _ _, λ H, ⟨λ x y y0,
   (H (x / y)).imp $ λ n h, le_of_lt $
   by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
 
@@ -247,8 +250,8 @@ begin
   cases exists_nat_gt (y - x)⁻¹ with n nh,
   cases exists_floor (x * n) with z zh,
   refine ⟨(z + 1 : ℤ) / n, _⟩,
-  have n0 := nat.cast_pos.1 (lt_trans (inv_pos.2 (sub_pos.2 h)) nh),
-  have n0' := (@nat.cast_pos α _ _).2 n0,
+  have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh,
+  have n0 := nat.cast_pos.1 n0',
   rw [rat.cast_div_of_ne_zero, rat.cast_coe_nat, rat.cast_coe_int, div_lt_iff n0'],
   refine ⟨(lt_div_iff n0').2 $
     (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩,

src/algebra/char_zero.lean

@@ -19,17 +19,15 @@ theorem char_zero_of_inj_zero {R : Type*} [add_left_cancel_monoid R] [has_one R]
 ⟨λ m n, begin
    assume h,
    wlog hle : m ≤ n,
-   cases nat.le.dest hle with k e,
-   suffices : k = 0, by rw [← e, this, add_zero],
-   apply H, apply @add_left_cancel R _ n,
-   rw [← h, ← nat.cast_add, e, add_zero, h]
+   rcases nat.le.dest hle with ⟨k, rfl⟩,
+   rw [nat.cast_add, eq_comm, add_eq_left_iff] at h,
+   rw [H k h, add_zero]
  end⟩
 
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_semiring.to_char_zero {R : Type*}
   [linear_ordered_semiring R] : char_zero R :=
-char_zero_of_inj_zero $ λ n h, nat.eq_zero_of_le_zero $
-  (@nat.cast_le R _ _ _).1 (le_of_eq h)
+⟨nat.strict_mono_cast.injective⟩
 
 namespace nat
 variables {R : Type*} [add_monoid R] [has_one R] [char_zero R]
@@ -61,13 +59,21 @@ end
 
 end nat
 
+section
+
+variables (M : Type*) [add_monoid M] [has_one M] [char_zero M]
+
 @[priority 100] -- see Note [lower instance priority]
-instance char_zero.infinite (α : Type*) [add_monoid α] [has_one α] [char_zero α] : infinite α :=
+instance char_zero.infinite : infinite M :=
 infinite.of_injective coe nat.cast_injective
 
-@[field_simps] lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=
-have ((2:ℕ):α) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
-by rwa [nat.cast_succ, nat.cast_one] at this
+variable {M}
+
+@[field_simps] lemma two_ne_zero' : (2:M) ≠ 0 :=
+have ((2:ℕ):M) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
+by rwa [nat.cast_two] at this
+
+end
 
 section
 variables {R : Type*} [semiring R] [no_zero_divisors R] [char_zero R]

src/algebra/group/basic.lean

@@ -107,25 +107,27 @@ end comm_monoid
 
 section left_cancel_monoid
 
-variables {M : Type u} [left_cancel_monoid M]
+variables {M : Type u} [left_cancel_monoid M] {a b : M}
 
-@[to_additive] lemma eq_one_of_mul_self_left_cancel {a : M} (h : a * a = a) : a = 1 :=
-mul_left_cancel (show a * a = a * 1, by rwa mul_one)
+@[simp, to_additive] lemma mul_eq_left_iff : a * b = a ↔ b = 1 :=
+calc a * b = a ↔ a * b = a * 1 : by rw mul_one
+           ... ↔ b = 1         : mul_left_cancel_iff
 
-@[to_additive] lemma eq_one_of_left_cancel_mul_self {a : M} (h : a = a * a) : a = 1 :=
-mul_left_cancel (show a * a = a * 1, by rwa [mul_one, eq_comm])
+@[simp, to_additive] lemma left_eq_mul_iff : a = a * b ↔ b = 1 :=
+eq_comm.trans mul_eq_left_iff
 
 end left_cancel_monoid
 
 section right_cancel_monoid
 
-variables {M : Type u} [right_cancel_monoid M]
+variables {M : Type u} [right_cancel_monoid M] {a b : M}
 
-@[to_additive] lemma eq_one_of_mul_self_right_cancel {a : M} (h : a * a = a) : a = 1 :=
-mul_right_cancel (show a * a = 1 * a, by rwa one_mul)
+@[simp, to_additive] lemma mul_eq_right_iff : a * b = b ↔ a = 1 :=
+calc a * b = b ↔ a * b = 1 * b : by rw one_mul
+           ... ↔ a = 1         : mul_right_cancel_iff
 
-@[to_additive] lemma eq_one_of_right_cancel_mul_self {a : M} (h : a = a * a) : a = 1 :=
-mul_right_cancel (show a * a = 1 * a, by rwa [one_mul, eq_comm])
+@[simp, to_additive] lemma right_eq_mul_iff : b = a * b ↔ a = 1 :=
+eq_comm.trans mul_eq_right_iff
 
 end right_cancel_monoid
 

src/algebra/group_power/basic.lean

@@ -526,8 +526,8 @@ by simpa only [one_pow] using pow_le_pow_of_le_left H n
 
 end canonically_ordered_semiring
 
-section linear_ordered_semiring
-variable [linear_ordered_semiring R]
+section ordered_semiring
+variable [ordered_semiring R]
 
 @[simp] theorem pow_pos {a : R} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
 | 0     := by { nontriviality, exact zero_lt_one }
@@ -548,43 +548,45 @@ begin
   { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
 end
 
-theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n)
-  (Hxyn : x ^ n = y ^ n) : x = y :=
-begin
-  rcases lt_trichotomy x y with hxy | rfl | hyx,
-  { exact absurd Hxyn (ne_of_lt (pow_lt_pow_of_lt_left hxy Hxpos Hnpos)) },
-  { refl },
-  { exact absurd Hxyn (ne_of_gt (pow_lt_pow_of_lt_left hyx Hypos Hnpos)) },
-end
+theorem strict_mono_incr_on_pow {n : ℕ} (hn : 0 < n) :
+  strict_mono_incr_on (λ x : R, x ^ n) (set.Ici 0) :=
+λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
 
 theorem one_le_pow_of_one_le {a : R} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | 0     := le_refl _
 | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
     zero_le_one (le_trans zero_le_one H)
 
+lemma pow_mono {a : R} (h : 1 ≤ a) : monotone (λ n : ℕ, a ^ n) :=
+monotone_of_monotone_nat $ λ n, le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h
+
 theorem pow_le_pow {a : R} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
-let ⟨k, hk⟩ := nat.le.dest h in
-calc a ^ n = a ^ n * 1 : (mul_one _).symm
-  ... ≤ a ^ n * a ^ k : mul_le_mul_of_nonneg_left
-    (one_le_pow_of_one_le ha _)
-    (pow_nonneg (le_trans zero_le_one ha) _)
-  ... = a ^ m : by rw [←hk, pow_add]
+pow_mono ha h
+
+lemma strict_mono_pow {a : R} (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
+have 0 < a := zero_le_one.trans_lt h,
+strict_mono.nat $ λ n, by simpa only [one_mul, pow_succ]
+  using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le
 
 lemma pow_lt_pow {a : R} {n m : ℕ} (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
-begin
-  have h' : 1 ≤ a := le_of_lt h,
-  have h'' : 0 < a := lt_trans zero_lt_one h,
-  cases m, cases h2, rw [pow_succ, ←one_mul (a ^ n)],
-  exact mul_lt_mul h (pow_le_pow h' (nat.le_of_lt_succ h2)) (pow_pos h'' _) (le_of_lt h'')
-end
+strict_mono_pow h h2
 
 lemma pow_lt_pow_iff {a : R} {n m : ℕ} (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
-strict_mono.lt_iff_lt $ λ m n, pow_lt_pow h
+(strict_mono_pow h).lt_iff_lt
 
 lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
 | 0     := by simp
 | (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)
 
+end ordered_semiring
+
+section linear_ordered_semiring
+variable [linear_ordered_semiring R]
+
+theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n)
+  (Hxyn : x ^ n = y ^ n) : x = y :=
+(@strict_mono_incr_on_pow R _ _ Hnpos).inj_on Hxpos Hypos Hxyn
+
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
 
@@ -597,10 +599,7 @@ theorem pow_two_nonneg [linear_ordered_ring R] (a : R) : 0 ≤ a ^ 2 :=
 by { rw pow_two, exact mul_self_nonneg _ }
 
 theorem pow_two_pos_of_ne_zero [linear_ordered_ring R] (a : R) (h : a ≠ 0) : 0 < a ^ 2 :=
-begin
-  nontriviality,
-  exact lt_of_le_of_ne (pow_two_nonneg a) (pow_ne_zero 2 h).symm
-end
+lt_of_le_of_ne (pow_two_nonneg a) (pow_ne_zero 2 h).symm
 
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]

src/algebra/group_power/lemmas.lean

@@ -283,8 +283,8 @@ by induction m with m ih; [exact int.cast_one,
 lemma neg_one_pow_eq_pow_mod_two [ring R] {n : ℕ} : (-1 : R) ^ n = (-1) ^ (n % 2) :=
 by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
 
-section linear_ordered_semiring
-variable [linear_ordered_semiring R]
+section ordered_semiring
+variable [ordered_semiring R]
 
 /-- Bernoulli's inequality. This version works for semirings but requires
 an additional hypothesis `0 ≤ a * a`. -/
@@ -339,7 +339,7 @@ lemma pow_le_one {x : R} : ∀ (n : ℕ) (h0 : 0 ≤ x) (h1 : x ≤ 1), x ^ n 
 | 0     h0 h1 := le_refl (1 : R)
 | (n+1) h0 h1 := mul_le_one h1 (pow_nonneg h0 _) (pow_le_one n h0 h1)
 
-end linear_ordered_semiring
+end ordered_semiring
 
 /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
 theorem one_add_mul_le_pow [linear_ordered_ring R] {a : R} (H : -2 ≤ a) :

src/data/int/cast.lean

@@ -125,35 +125,49 @@ by rw [bit1, cast_add, cast_one, cast_bit0]; refl
 
 lemma cast_two [ring α] : ((2 : ℤ) : α) = 2 := by simp
 
-theorem cast_nonneg [linear_ordered_ring α] : ∀ {n : ℤ}, (0 : α) ≤ n ↔ 0 ≤ n
+theorem cast_mono [ordered_ring α] : monotone (coe : ℤ → α) :=
+begin
+  intros m n h,
+  rw ← sub_nonneg at h,
+  lift n - m to ℕ using h with k,
+  rw [← sub_nonneg, ← cast_sub, ← h_1, cast_coe_nat],
+  exact k.cast_nonneg
+end
+
+@[simp] theorem cast_nonneg [ordered_ring α] [nontrivial α] : ∀ {n : ℤ}, (0 : α) ≤ n ↔ 0 ≤ n
 | (n : ℕ) := by simp
-| -[1+ n] := by simpa [not_le_of_gt (neg_succ_lt_zero n)] using
-             show -(n:α) < 1, from lt_of_le_of_lt (by simp) zero_lt_one
+| -[1+ n] := have -(n:α) < 1, from lt_of_le_of_lt (by simp) zero_lt_one,
+             by simpa [(neg_succ_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le
 
-@[simp, norm_cast] theorem cast_le [linear_ordered_ring α] {m n : ℤ} : (m : α) ≤ n ↔ m ≤ n :=
+@[simp, norm_cast] theorem cast_le [ordered_ring α] [nontrivial α] {m n : ℤ} :
+  (m : α) ≤ n ↔ m ≤ n :=
 by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
 
-@[simp, norm_cast] theorem cast_lt [linear_ordered_ring α] {m n : ℤ} : (m : α) < n ↔ m < n :=
-by simpa [-cast_le] using not_congr (@cast_le α _ n m)
+theorem cast_strict_mono [ordered_ring α] [nontrivial α] : strict_mono (coe : ℤ → α) :=
+strict_mono_of_le_iff_le $ λ m n, cast_le.symm
+
+@[simp, norm_cast] theorem cast_lt [ordered_ring α] [nontrivial α] {m n : ℤ} :
+  (m : α) < n ↔ m < n :=
+cast_strict_mono.lt_iff_lt
 
-@[simp] theorem cast_nonpos [linear_ordered_ring α] {n : ℤ} : (n : α) ≤ 0 ↔ n ≤ 0 :=
+@[simp] theorem cast_nonpos [ordered_ring α] [nontrivial α] {n : ℤ} : (n : α) ≤ 0 ↔ n ≤ 0 :=
 by rw [← cast_zero, cast_le]
 
-@[simp] theorem cast_pos [linear_ordered_ring α] {n : ℤ} : (0 : α) < n ↔ 0 < n :=
+@[simp] theorem cast_pos [ordered_ring α] [nontrivial α] {n : ℤ} : (0 : α) < n ↔ 0 < n :=
 by rw [← cast_zero, cast_lt]
 
-@[simp] theorem cast_lt_zero [linear_ordered_ring α] {n : ℤ} : (n : α) < 0 ↔ n < 0 :=
+@[simp] theorem cast_lt_zero [ordered_ring α] [nontrivial α] {n : ℤ} : (n : α) < 0 ↔ n < 0 :=
 by rw [← cast_zero, cast_lt]
 
-@[simp, norm_cast] theorem cast_min [linear_ordered_comm_ring α] {a b : ℤ} :
+@[simp, norm_cast] theorem cast_min [linear_ordered_ring α] {a b : ℤ} :
   (↑(min a b) : α) = min a b :=
-by by_cases a ≤ b; simp [h, min]
+monotone.map_min cast_mono
 
-@[simp, norm_cast] theorem cast_max [linear_ordered_comm_ring α] {a b : ℤ} :
+@[simp, norm_cast] theorem cast_max [linear_ordered_ring α] {a b : ℤ} :
   (↑(max a b) : α) = max a b :=
-by by_cases b ≤ a; simp [h, max]
+monotone.map_max cast_mono
 
-@[simp, norm_cast] theorem cast_abs [linear_ordered_comm_ring α] {q : ℤ} :
+@[simp, norm_cast] theorem cast_abs [linear_ordered_ring α] {q : ℤ} :
   ((abs q : ℤ) : α) = abs q :=
 by simp [abs]
 

src/data/nat/cast.lean

@@ -83,7 +83,7 @@ def cast_add_monoid_hom (α : Type*) [add_monoid α] [has_one α] : ℕ →+ α
   ((bit1 n : ℕ) : α) = bit1 n :=
 by rw [bit1, cast_add_one, cast_bit0]; refl
 
-lemma cast_two {α : Type*} [semiring α] : ((2 : ℕ) : α) = 2 := by simp
+lemma cast_two {α : Type*} [add_monoid α] [has_one α] : ((2 : ℕ) : α) = 2 := by simp
 
 @[simp, norm_cast] theorem cast_pred [add_group α] [has_one α] :
   ∀ {n}, 0 < n → ((n - 1 : ℕ) : α) = n - 1
@@ -121,38 +121,50 @@ nat.rec_on n (commute.zero_left x) $ λ n ihn, ihn.add_left $ commute.one_left x
 lemma commute_cast [semiring α] (x : α) (n : ℕ) : commute x n :=
 (n.cast_commute x).symm
 
-@[simp] theorem cast_nonneg [linear_ordered_semiring α] : ∀ n : ℕ, 0 ≤ (n : α)
+section
+
+variables [ordered_semiring α]
+
+@[simp] theorem cast_nonneg : ∀ n : ℕ, 0 ≤ (n : α)
 | 0     := le_refl _
 | (n+1) := add_nonneg (cast_nonneg n) zero_le_one
 
-theorem strict_mono_cast [linear_ordered_semiring α] : strict_mono (coe : ℕ → α) :=
+theorem mono_cast : monotone (coe : ℕ → α) :=
+λ m n h, let ⟨k, hk⟩ := le_iff_exists_add.1 h in by simp [hk]
+
+variable [nontrivial α]
+
+theorem strict_mono_cast : strict_mono (coe : ℕ → α) :=
 λ m n h, nat.le_induction (lt_add_of_pos_right _ zero_lt_one)
   (λ n _ h, lt_add_of_lt_of_pos h zero_lt_one) _ h
 
-@[simp, norm_cast] theorem cast_le [linear_ordered_semiring α] {m n : ℕ} : (m : α) ≤ n ↔ m ≤ n :=
+@[simp, norm_cast] theorem cast_le {m n : ℕ} :
+  (m : α) ≤ n ↔ m ≤ n :=
 strict_mono_cast.le_iff_le
 
-@[simp, norm_cast] theorem cast_lt [linear_ordered_semiring α] {m n : ℕ} : (m : α) < n ↔ m < n :=
+@[simp, norm_cast] theorem cast_lt {m n : ℕ} : (m : α) < n ↔ m < n :=
 strict_mono_cast.lt_iff_lt
 
-@[simp] theorem cast_pos [linear_ordered_semiring α] {n : ℕ} : (0 : α) < n ↔ 0 < n :=
+@[simp] theorem cast_pos {n : ℕ} : (0 : α) < n ↔ 0 < n :=
 by rw [← cast_zero, cast_lt]
 
-lemma cast_add_one_pos [linear_ordered_semiring α] (n : ℕ) : 0 < (n : α) + 1 :=
+lemma cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 :=
   add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one
 
-@[simp, norm_cast] theorem one_lt_cast [linear_ordered_semiring α] {n : ℕ} : 1 < (n : α) ↔ 1 < n :=
+@[simp, norm_cast] theorem one_lt_cast {n : ℕ} : 1 < (n : α) ↔ 1 < n :=
 by rw [← cast_one, cast_lt]
 
-@[simp, norm_cast] theorem one_le_cast [linear_ordered_semiring α] {n : ℕ} : 1 ≤ (n : α) ↔ 1 ≤ n :=
+@[simp, norm_cast] theorem one_le_cast {n : ℕ} : 1 ≤ (n : α) ↔ 1 ≤ n :=
 by rw [← cast_one, cast_le]
 
-@[simp, norm_cast] theorem cast_lt_one [linear_ordered_semiring α] {n : ℕ} : (n : α) < 1 ↔ n = 0 :=
+@[simp, norm_cast] theorem cast_lt_one {n : ℕ} : (n : α) < 1 ↔ n = 0 :=
 by rw [← cast_one, cast_lt, lt_succ_iff, le_zero_iff]
 
-@[simp, norm_cast] theorem cast_le_one [linear_ordered_semiring α] {n : ℕ} : (n : α) ≤ 1 ↔ n ≤ 1 :=
+@[simp, norm_cast] theorem cast_le_one {n : ℕ} : (n : α) ≤ 1 ↔ n ≤ 1 :=
 by rw [← cast_one, cast_le]
 
+end
+
 @[simp, norm_cast] theorem cast_min [linear_ordered_semiring α] {a b : ℕ} :
   (↑(min a b) : α) = min a b :=
 by by_cases a ≤ b; simp [h, min]
@@ -161,7 +173,7 @@ by by_cases a ≤ b; simp [h, min]
   (↑(max a b) : α) = max a b :=
 by by_cases a ≤ b; simp [h, max]
 
-@[simp, norm_cast] theorem abs_cast [linear_ordered_comm_ring α] (a : ℕ) :
+@[simp, norm_cast] theorem abs_cast [linear_ordered_ring α] (a : ℕ) :
   abs (a : α) = a :=
 abs_of_nonneg (cast_nonneg a)