chore(src/algebra/ordered_ring.lean): fix linting errors (#2827)

[Mentioned, but not really discussed, in this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20get.20familiar.20enough.20with.20Mathlib.20to.20use.20it/near/198747067).

This PR also removes `mul_pos'` and `mul_nonneg'` lemmas because they are now identical to the improved `mul_pos` and `mul_nonneg`.

Author: Vierkantor

src/algebra/ordered_ring.lean

@@ -12,6 +12,8 @@ set_option old_structure_cmd true
 universe u
 variable {α : Type u}
 
+/-- An `ordered_semiring α` is a semiring `α` with a partial order such that
+multiplication with a positive number and addition are monotone. -/
 class ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_comm_monoid α :=
 (mul_lt_mul_of_pos_left :  ∀ a b c : α, a < b → 0 < c → c * a < c * b)
 (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
@@ -53,15 +55,10 @@ calc
   a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b
     ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c
 
-lemma mul_nonneg (ha : a ≥ 0) (hb : b ≥ 0) : a * b ≥ 0 :=
+lemma mul_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
 have h : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right ha hb,
 by rwa [zero_mul] at h
 
--- `mul_nonneg` and `mul_pos` in core are stated in terms of `≥` and `>`, so we restate them here
--- for use in syntactic tactics (e.g. `simp` and `rw`).
-lemma mul_nonneg' : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
-mul_nonneg
-
 lemma mul_nonpos_of_nonneg_of_nonpos (ha : a ≥ 0) (hb : b ≤ 0) : a * b ≤ 0 :=
 have h : a * b ≤ a * 0, from mul_le_mul_of_nonneg_left hb ha,
 by rwa mul_zero at h
@@ -80,13 +77,10 @@ calc
    a * b ≤ c * b : mul_le_mul_of_nonneg_right h1 h3
      ... < c * d : mul_lt_mul_of_pos_left h2 h4
 
-lemma mul_pos (ha : a > 0) (hb : b > 0) : a * b > 0 :=
+lemma mul_pos (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
 have h : 0 * b < a * b, from mul_lt_mul_of_pos_right ha hb,
 by rwa zero_mul at h
 
-lemma mul_pos' (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
-mul_pos ha hb
-
 lemma mul_neg_of_pos_of_neg (ha : a > 0) (hb : b < 0) : a * b < 0 :=
 have h : a * b < a * 0, from mul_lt_mul_of_pos_left hb ha,
 by rwa mul_zero at h
@@ -103,6 +97,8 @@ mul_lt_mul' (le_of_lt h2) h2 h1 (lt_of_le_of_lt h1 h2)
 
 end ordered_semiring
 
+/-- A `linear_ordered_semiring α` is a semiring `α` with a linear order
+such that multiplication with a positive number and addition are monotone. -/
 class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_order α :=
 (zero_lt_one : zero < one)
 
@@ -120,14 +116,14 @@ lemma two_pos : 0 < (2:α) := add_pos zero_lt_one zero_lt_one
 @[field_simps] lemma two_ne_zero : (2:α) ≠ 0 :=
 ne.symm (ne_of_lt two_pos)
 
-lemma two_gt_one : (2:α) > 1 :=
+lemma two_gt_one : 1 < (2:α) :=
 calc (2:α) = 1+1 : one_add_one_eq_two
      ...   > 1+0 : add_lt_add_left zero_lt_one _
      ...   = 1   : add_zero 1
 
-lemma two_ge_one : (2:α) ≥ 1 := le_of_lt two_gt_one
+lemma two_ge_one : 1 ≤ (2:α) := le_of_lt two_gt_one
 
-lemma four_pos : (4:α) > 0 := add_pos two_pos two_pos
+lemma four_pos : 0 < (4:α) := add_pos two_pos two_pos
 
 lemma lt_of_mul_lt_mul_left (h : c * a < c * b) (hc : c ≥ 0) : a < b :=
 lt_of_not_ge
@@ -415,7 +411,10 @@ lemma strict_mono.mul (hf : strict_mono f) (hg : strict_mono g) (hf0 : ∀ x, 0
 
 end mono
 
-class decidable_linear_ordered_semiring (α : Type u) extends linear_ordered_semiring α, decidable_linear_order α
+/-- A `decidable_linear_ordered_semiring α` is a semiring `α` with a decidable linear order
+such that multiplication with a positive number and addition are monotone. -/
+class decidable_linear_ordered_semiring (α : Type u)
+  extends linear_ordered_semiring α, decidable_linear_order α
 
 section decidable_linear_ordered_semiring
 variables [decidable_linear_ordered_semiring α] {a b c : α}
@@ -428,6 +427,8 @@ decidable.le_iff_le_iff_lt_iff_lt.2 $ mul_lt_mul_right h
 
 end decidable_linear_ordered_semiring
 
+/-- An `ordered_ring α` is a ring `α` with a partial order such that
+multiplication with a positive number and addition are monotone. -/
 class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α, zero_ne_one_class α :=
 (mul_pos    : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
 
@@ -517,6 +518,8 @@ by rwa zero_mul at this
 
 end ordered_ring
 
+/-- A `linear_ordered_ring α` is a ring `α` with a linear order such that
+multiplication with a positive number and addition are monotone. -/
 class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_order α :=
 (zero_lt_one : zero < one)
 
@@ -534,13 +537,13 @@ instance linear_ordered_ring.to_linear_ordered_semiring : linear_ordered_semirin
   le_total                   := linear_ordered_ring.le_total,
   ..‹linear_ordered_ring α› }
 
-lemma mul_self_nonneg (a : α) : a * a ≥ 0 :=
+lemma mul_self_nonneg (a : α) : 0 ≤ a * a :=
 or.elim (le_total 0 a)
   (assume h : a ≥ 0, mul_nonneg h h)
   (assume h : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos h h)
 
-lemma pos_and_pos_or_neg_and_neg_of_mul_pos (hab : a * b > 0) :
-    (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
+lemma pos_and_pos_or_neg_and_neg_of_mul_pos (hab : 0 < a * b) :
+    (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) :=
 match lt_trichotomy 0 a with
 | or.inl hlt₁          :=
   match lt_trichotomy 0 b with
@@ -557,8 +560,8 @@ match lt_trichotomy 0 a with
   end
 end
 
-lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : a > b :=
-have nhc : -c ≥ 0, from neg_nonneg_of_nonpos hc,
+lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
+have nhc : 0 ≤ -c, from neg_nonneg_of_nonpos hc,
 have h2 : -(c * b) < -(c * a), from neg_lt_neg h,
 have h3 : (-c) * b < (-c) * a, from calc
      (-c) * b = - (c * b)    : by rewrite neg_mul_eq_neg_mul
@@ -676,12 +679,17 @@ end
 
 end linear_ordered_ring
 
+/-- A `linear_ordered_comm_ring α` is a commutative ring `α` with a linear order
+such that multiplication with a positive number and addition are monotone. -/
 class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α
 
 instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _,
   ..s }
 
+/-- A `decidable_linear_ordered_comm_ring α` is a commutative ring `α` with a
+decidable linear order such that multiplication with a positive number and
+addition are monotone. -/
 class decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_comm_ring α,
     decidable_linear_ordered_add_comm_group α
 
@@ -827,6 +835,8 @@ instance to_ordered_ring : ordered_ring α :=
   mul_pos := λ a b, by simp [pos_def.symm]; exact mul_pos,
   ..‹nonneg_ring α› }
 
+/-- `to_linear_nonneg_ring` shows that a `nonneg_ring` with a total order is a `domain`,
+hence a `linear_nonneg_ring`. -/
 def to_linear_nonneg_ring
   (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
   : linear_nonneg_ring α :=
@@ -907,6 +917,9 @@ def to_decidable_linear_ordered_comm_ring
 
 end linear_nonneg_ring
 
+/-- A canonically ordered commutative semiring is an ordered, commutative semiring
+in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by the
+natural numbers, for example, but not the integers or other ordered groups. -/
 class canonically_ordered_comm_semiring (α : Type*) extends
   canonically_ordered_add_monoid α, comm_semiring α, zero_ne_one_class α :=
 (mul_eq_zero_iff (a b : α) : a * b = 0 ↔ a = 0 ∨ b = 0)
@@ -935,31 +948,33 @@ by simp only [zero_lt_iff_ne_zero, ne.def, canonically_ordered_comm_semiring.mul
 end canonically_ordered_semiring
 
 namespace with_top
-variables [canonically_ordered_comm_semiring α] [decidable_eq α]
-
-instance : mul_zero_class (with_top α) :=
-{ zero := 0,
-  mul := λm n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
-  zero_mul := assume a, if_pos $ or.inl rfl,
-  mul_zero := assume a, if_pos $ or.inr rfl }
+variables [canonically_ordered_comm_semiring α]
 
 instance : has_one (with_top α) := ⟨↑(1:α)⟩
 
-lemma mul_def {a b : with_top α} :
-  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
-
-@[simp] theorem top_ne_zero [partial_order α] : ⊤ ≠ (0 : with_top α) .
-@[simp] theorem zero_ne_top [partial_order α] : (0 : with_top α) ≠ ⊤ .
+@[simp] theorem top_ne_zero : ⊤ ≠ (0 : with_top α) .
+@[simp] theorem zero_ne_top : (0 : with_top α) ≠ ⊤ .
 
-@[simp] theorem coe_eq_zero [partial_order α] {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
+@[simp] theorem coe_eq_zero {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
 iff.intro
   (assume h, match a, h with _, rfl := rfl end)
   (assume h, h.symm ▸ rfl)
 
-@[simp] theorem zero_eq_coe [partial_order α] {a : α} : 0 = (a : with_top α) ↔ a = 0 :=
+@[simp] theorem zero_eq_coe {a : α} : 0 = (a : with_top α) ↔ a = 0 :=
 by rw [eq_comm, coe_eq_zero]
 
-@[simp] theorem coe_zero [partial_order α] : ↑(0 : α) = (0 : with_top α) := rfl
+@[simp] theorem coe_zero : ↑(0 : α) = (0 : with_top α) := rfl
+
+variable [decidable_eq α]
+
+instance : mul_zero_class (with_top α) :=
+{ zero := 0,
+  mul := λm n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
+  zero_mul := assume a, if_pos $ or.inl rfl,
+  mul_zero := assume a, if_pos $ or.inr rfl }
+
+lemma mul_def {a b : with_top α} :
+  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
 
 @[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ :=
 by cases a; simp [mul_def, h]; refl
@@ -1029,8 +1044,7 @@ private lemma one_mul' : ∀a : with_top α, 1 * a = a
 | none     := show ((1:α) : with_top α) * ⊤ = ⊤, by simp [-with_bot.coe_one]
 | (some a) := show ((1:α) : with_top α) * a = a, by simp [coe_mul.symm, -with_bot.coe_one]
 
-instance [canonically_ordered_comm_semiring α] [decidable_eq α] :
-  canonically_ordered_comm_semiring (with_top α) :=
+instance : canonically_ordered_comm_semiring (with_top α) :=
 { one             := (1 : α),
   right_distrib   := distrib',
   left_distrib    := assume a b c, by rw [comm, distrib', comm b, comm c]; refl,

src/analysis/analytic/basic.lean

@@ -620,7 +620,7 @@ begin
   have A_nonneg : ∀ i, 0 ≤ A i,
   { rintros ⟨k, n, s, hs⟩,
     change 0 ≤ ∥(p n).restr s hs x∥ * (r : ℝ) ^ k,
-    refine mul_nonneg' (norm_nonneg _) (pow_nonneg (nnreal.coe_nonneg _) _) },
+    refine mul_nonneg (norm_nonneg _) (pow_nonneg (nnreal.coe_nonneg _) _) },
   have tsum_nonneg : 0 ≤ tsum A := tsum_nonneg A_nonneg,
   apply le_radius_of_bound _ (nnreal.of_real (tsum A)) (λ k, _),
   rw [← nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_pow, coe_nnnorm,

src/analysis/analytic/composition.lean

@@ -362,9 +362,9 @@ begin
   let r0 : nnreal := (4 * max Cp 1)⁻¹,
   set r := min rp 1 * min rq 1 * r0,
   have r_pos : 0 < r,
-  { apply mul_pos' (mul_pos' _ _),
+  { apply mul_pos (mul_pos _ _),
     { rw [nnreal.inv_pos],
-      apply mul_pos',
+      apply mul_pos,
       { norm_num },
       { exact lt_of_lt_of_le zero_lt_one (le_max_right _ _) } },
     { rw ennreal.coe_pos at rp_pos, simp [rp_pos, zero_lt_one] },

src/analysis/normed_space/basic.lean

@@ -564,7 +564,7 @@ begin
   refine (nhds_basis_closed_ball.tendsto_iff nhds_basis_closed_ball).2 (λε εpos, _),
   let δ := min (ε/2 * ∥r∥^2) (∥r∥/2),
   have norm_r_pos : 0 < ∥r∥ := norm_pos_iff.mpr r0,
-  have A : 0 < ε / 2 * ∥r∥ ^ 2 := mul_pos' (half_pos εpos) (pow_pos norm_r_pos 2),
+  have A : 0 < ε / 2 * ∥r∥ ^ 2 := mul_pos (half_pos εpos) (pow_pos norm_r_pos 2),
   have δpos : 0 < δ, by simp [half_pos norm_r_pos, A],
   refine ⟨δ, δpos, λ x hx, _⟩,
   have rx : ∥r∥/2 ≤ ∥x∥ := calc

src/analysis/normed_space/bounded_linear_maps.lean

@@ -187,7 +187,7 @@ begin
   refine is_linear_map.with_bound ⟨λ f₁ f₂, by { ext m, refl }, λ c f, by { ext m, refl }⟩
     (∥g∥ ^ (fintype.card ι)) (λ f, _),
   apply continuous_multilinear_map.op_norm_le_bound _ _ (λ m, _),
-  { apply_rules [mul_nonneg', pow_nonneg, norm_nonneg, norm_nonneg] },
+  { apply_rules [mul_nonneg, pow_nonneg, norm_nonneg, norm_nonneg] },
   calc ∥f (g ∘ m)∥ ≤
     ∥f∥ * finset.univ.prod (λ (i : ι), ∥g (m i)∥) : f.le_op_norm _
     ... ≤ ∥f∥ * finset.univ.prod (λ (i : ι), ∥g∥ * ∥m i∥) : begin
@@ -248,11 +248,11 @@ lemma is_bounded_bilinear_map.is_bounded_linear_map_left (h : is_bounded_bilinea
   smul  := λ c x, h.smul_left _ _ _,
   bound := begin
     rcases h.bound with ⟨C, C_pos, hC⟩,
-    refine ⟨C * (∥y∥ + 1), mul_pos' C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ x, _⟩,
+    refine ⟨C * (∥y∥ + 1), mul_pos C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ x, _⟩,
     have : ∥y∥ ≤ ∥y∥ + 1, by simp [zero_le_one],
     calc ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥ : hC x y
     ... ≤ C * ∥x∥ * (∥y∥ + 1) :
-      by apply_rules [norm_nonneg, mul_le_mul_of_nonneg_left, le_of_lt C_pos, mul_nonneg']
+      by apply_rules [norm_nonneg, mul_le_mul_of_nonneg_left, le_of_lt C_pos, mul_nonneg]
     ... = C * (∥y∥ + 1) * ∥x∥ : by ring
   end }
 
@@ -262,7 +262,7 @@ lemma is_bounded_bilinear_map.is_bounded_linear_map_right (h : is_bounded_biline
   smul  := λ c y, h.smul_right _ _ _,
   bound := begin
     rcases h.bound with ⟨C, C_pos, hC⟩,
-    refine ⟨C * (∥x∥ + 1), mul_pos' C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ y, _⟩,
+    refine ⟨C * (∥x∥ + 1), mul_pos C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ y, _⟩,
     have : ∥x∥ ≤ ∥x∥ + 1, by simp [zero_le_one],
     calc ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥ : hC x y
     ... ≤ C * (∥x∥ + 1) * ∥y∥ :

src/analysis/normed_space/multilinear.lean

@@ -110,7 +110,7 @@ begin
   by_cases h : ∃i, m i = 0,
   { rcases h with ⟨i, hi⟩,
     rw [f.map_coord_zero i hi, _root_.norm_zero],
-    exact mul_nonneg' (le_of_lt C_pos) (prod_nonneg (λi hi, norm_nonneg _)) },
+    exact mul_nonneg (le_of_lt C_pos) (prod_nonneg (λi hi, norm_nonneg _)) },
   { push_neg at h,
     have : ∀i, ∃d:𝕜, d ≠ 0 ∧ ∥d • m i∥ ≤ δ ∧ (δ/∥c∥ ≤ ∥d • m i∥) ∧ (∥d∥⁻¹ ≤ δ⁻¹ * ∥c∥ * ∥m i∥) :=
       λi, rescale_to_shell hc δ_pos (h i),
@@ -233,7 +233,7 @@ begin
     ≤ D * (fintype.card ι) * (max ∥m'∥ ∥m∥) ^ (fintype.card ι - 1) * ∥m' - m∥ :
       f.norm_image_sub_le_of_bound D_pos H m' m
     ... ≤ D * (fintype.card ι) * (∥m∥ + 1) ^ (fintype.card ι - 1) * ∥m' - m∥ :
-      by apply_rules [mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, mul_nonneg',
+      by apply_rules [mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, mul_nonneg,
         norm_nonneg, nat.cast_nonneg, pow_le_pow_of_le_left]
 end
 
@@ -326,7 +326,7 @@ begin
     rw norm_eq_zero at hi,
     have : f m = 0 := f.map_coord_zero i hi,
     rw [this, norm_zero],
-    exact mul_nonneg' (op_norm_nonneg f) A },
+    exact mul_nonneg (op_norm_nonneg f) A },
   { have hlt : 0 < finset.univ.prod (λi, ∥m i∥) := lt_of_le_of_ne A (ne.symm h),
     exact le_mul_of_div_le hlt ((le_Inf _ bounds_nonempty bounds_bdd_below).2
       (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (begin rw mul_comm, apply hc, end))) }
@@ -434,7 +434,7 @@ begin
     ... ≤ (∥p∥ + 1) * (fintype.card ι) * (∥p∥ + 1) ^ (fintype.card ι - 1) * ∥q - p∥
           + ∥q - p∥ * univ.prod (λi, ∥p.2 i∥) :
       by apply_rules [add_le_add, mul_le_mul, le_refl, le_trans (norm_fst_le q) A, nat.cast_nonneg,
-        mul_nonneg', pow_le_pow_of_le_left, pow_nonneg, norm_snd_le (q - p), norm_nonneg,
+        mul_nonneg, pow_le_pow_of_le_left, pow_nonneg, norm_snd_le (q - p), norm_nonneg,
         norm_fst_le (q - p), norm_nonneg, prod_nonneg]
     ... = ((∥p∥ + 1) * (fintype.card ι) * (∥p∥ + 1) ^ (fintype.card ι - 1)
               + univ.prod (λi, ∥p.2 i∥)) * dist q p : by { rw dist_eq_norm, ring }
@@ -707,7 +707,7 @@ linear_map.mk_continuous
   add    := λx y, by { ext m, exact f.cons_add m x y },
   smul   := λc x, by { ext m, exact f.cons_smul m c x } }
   -- then register its continuity thanks to its boundedness properties.
-(∥f∥) (λx, multilinear_map.mk_continuous_norm_le _ (mul_nonneg' (norm_nonneg _) (norm_nonneg _)) _)
+(∥f∥) (λx, multilinear_map.mk_continuous_norm_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _)
 
 @[simp] lemma continuous_multilinear_map.curry_left_apply
   (f : continuous_multilinear_map 𝕜 E E₂) (x : E 0) (m : Π(i : fin n), E i.succ) :
@@ -835,7 +835,7 @@ let f' : multilinear_map 𝕜 (λ(i : fin n), E i.cast_succ) (E (last n) →L[
   add  := λ m i x y, by { simp, refl },
   smul := λ m i c x, by { simp, refl } } in
 f'.mk_continuous (∥f∥) (λm, linear_map.mk_continuous_norm_le _
-  (mul_nonneg' (norm_nonneg _) (prod_nonneg (λj hj, norm_nonneg _))) _)
+  (mul_nonneg (norm_nonneg _) (prod_nonneg (λj hj, norm_nonneg _))) _)
 
 @[simp] lemma continuous_multilinear_map.curry_right_apply
   (f : continuous_multilinear_map 𝕜 E E₂) (m : Π(i : fin n), E i.cast_succ) (x : E (last n)) :

src/analysis/normed_space/operator_norm.lean

@@ -120,7 +120,7 @@ begin
     { assume x,
       by_cases hx : f x = 0,
       { rw [hx, norm_zero],
-        apply_rules [mul_nonneg', norm_nonneg, inv_nonneg.2, norm_nonneg] },
+        apply_rules [mul_nonneg, norm_nonneg, inv_nonneg.2, norm_nonneg] },
       { let y := x₀ - (f x₀ * (f x)⁻¹ ) • x,
         have fy_zero : f y = 0, by calc
           f y = f x₀ - (f x₀ * (f x)⁻¹ ) * f x : by simp [y]
@@ -135,7 +135,7 @@ begin
           ∥f x∥ = (r * ∥x₀∥)⁻¹ * (r * ∥x₀∥) * ∥f x∥ : by rwa [inv_mul_cancel, one_mul]
           ... ≤ (r * ∥x₀∥)⁻¹ * (∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥) * ∥f x∥ : begin
             apply mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left A _) (norm_nonneg _),
-            exact inv_nonneg.2 (mul_nonneg' (by norm_num) (norm_nonneg _))
+            exact inv_nonneg.2 (mul_nonneg (by norm_num) (norm_nonneg _))
           end
           ... = (∥f x∥ ⁻¹ * ∥f x∥) * (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ : by ring
           ... = (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ :

src/data/rat/order.lean

@@ -47,7 +47,7 @@ num_denom_cases_on' b $ λ n₂ d₂ h₂,
 begin
   have d₁0 : 0 < (d₁:ℤ) := int.coe_nat_pos.2 (nat.pos_of_ne_zero h₁),
   have d₂0 : 0 < (d₂:ℤ) := int.coe_nat_pos.2 (nat.pos_of_ne_zero h₂),
-  simp [d₁0, d₂0, h₁, h₂, mul_pos' d₁0 d₂0],
+  simp [d₁0, d₂0, h₁, h₂, mul_pos d₁0 d₂0],
   intros n₁0 n₂0,
   apply add_nonneg; apply mul_nonneg; {assumption <|> apply int.coe_zero_le},
 end
@@ -58,7 +58,7 @@ num_denom_cases_on' b $ λ n₂ d₂ h₂,
 begin
   have d₁0 : 0 < (d₁:ℤ) := int.coe_nat_pos.2 (nat.pos_of_ne_zero h₁),
   have d₂0 : 0 < (d₂:ℤ) := int.coe_nat_pos.2 (nat.pos_of_ne_zero h₂),
-  simp [d₁0, d₂0, h₁, h₂, mul_pos' d₁0 d₂0],
+  simp [d₁0, d₂0, h₁, h₂, mul_pos d₁0 d₂0],
   exact mul_nonneg
 end
 
@@ -89,7 +89,7 @@ protected theorem le_def {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
 begin
   show rat.nonneg _ ↔ _,
   rw ← sub_nonneg,
-  simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, mul_pos' d0 b0]
+  simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, mul_pos d0 b0]
 end
 
 protected theorem le_refl : a ≤ a :=