feat: deprecate div_le_div_of_le_of_nonneg (#9399)

This was noticed in the discussion around #9393.

Mathlib/Algebra/Order/Field/Basic.lean

@@ -351,6 +351,7 @@ theorem div_le_div_of_le_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b
   exact mul_le_mul_of_nonneg_left ((inv_le_inv (hc.trans_le h) hc).mpr h) ha
 #align div_le_div_of_le_left div_le_div_of_le_left
 
+@[deprecated div_le_div_of_le]
 theorem div_le_div_of_le_of_nonneg (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c :=
   div_le_div_of_le hc hab
 #align div_le_div_of_le_of_nonneg div_le_div_of_le_of_nonneg

Mathlib/Algebra/Order/Floor.lean

@@ -540,7 +540,7 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   refine' (floor_eq_iff _).2 _
   · exact div_nonneg ha n.cast_nonneg
   constructor
-  · exact cast_div_le.trans (div_le_div_of_le_of_nonneg (floor_le ha) n.cast_nonneg)
+  · exact cast_div_le.trans (div_le_div_of_le n.cast_nonneg (floor_le ha))
   rw [div_lt_iff, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]
   · exact lt_div_mul_add hn
   · exact cast_pos.2 hn

Mathlib/Analysis/Calculus/Monotone.lean

@@ -171,11 +171,11 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
     · filter_upwards [self_mem_nhdsWithin]
       rintro y (hy : x < y)
       have : ↑0 < (y - x) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
-      apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
+      apply div_le_div_of_le (sub_pos.2 hy).le
       exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
     · filter_upwards [self_mem_nhdsWithin]
       rintro y (hy : x < y)
-      apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
+      apply div_le_div_of_le (sub_pos.2 hy).le
       exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl y))
   -- prove differentiability on the left, by sandwiching with values of `g`
   have L2 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x)

Mathlib/Analysis/NormedSpace/AddTorsor.lean

@@ -214,7 +214,7 @@ theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
   rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
   try infer_instance
   rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
-  exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _)
+  exact div_le_div_of_le (norm_nonneg _) (norm_add_le _ _)
 #align dist_midpoint_midpoint_le' dist_midpoint_midpoint_le'
 
 theorem nndist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :

Mathlib/Combinatorics/Additive/Behrend.lean

@@ -333,7 +333,7 @@ theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x
     rw [← add_assoc, sub_add_cancel]
     linarith
   refine' lt_of_le_of_lt _ (div_lt_div_of_lt_left (exp_pos _) (cast_pos.2 <| ceil_pos.2 hx) h₁)
-  refine' le_trans _ (div_le_div_of_le_of_nonneg (exp_le_exp.2 h₂) <| add_nonneg hx.le zero_le_one)
+  refine' le_trans _ (div_le_div_of_le (add_nonneg hx.le zero_le_one) (exp_le_exp.2 h₂))
   rw [le_div_iff (add_pos hx zero_lt_one), ← le_div_iff' (exp_pos _), ← exp_sub, neg_mul,
     sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]
   exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -396,7 +396,7 @@ private theorem eps_le_card_star_div [Nonempty α] (hPα : P.parts.card * 16 ^ P
   calc
     4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
     _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * ((G.nonuniformWitness ε U V).card / U.card) :=
-      (mul_le_mul (mul_le_mul (sub_le_sub_left (div_le_div_of_le_of_nonneg hε₁ <| by norm_num) _)
+      (mul_le_mul (mul_le_mul (sub_le_sub_left (div_le_div_of_le (by norm_num) hε₁) _)
         (sub_le_sub_left (inv_le_inv_of_le (by norm_num) <|
           mod_cast (show 9 ≤ 100 by norm_num).trans
             (hundred_le_m hPα hPε hε₁)) _) (by norm_num) hε)
@@ -462,8 +462,8 @@ private theorem edgeDensity_star_not_uniform [Nonempty α]
     exact this
   have hε' : ε ^ 5 ≤ ε := by
     simpa using pow_le_pow_of_le_one (by sz_positivity) hε₁ (show 1 ≤ 5 by norm_num)
-  have hpr' : |p - r| ≤ ε / 49 := hpr.trans (div_le_div_of_le_of_nonneg hε' <| by norm_num)
-  have hqt' : |q - t| ≤ ε / 49 := hqt.trans (div_le_div_of_le_of_nonneg hε' <| by norm_num)
+  have hpr' : |p - r| ≤ ε / 49 := hpr.trans (div_le_div_of_le (by norm_num) hε')
+  have hqt' : |q - t| ≤ ε / 49 := hqt.trans (div_le_div_of_le (by norm_num) hε')
   rw [abs_sub_le_iff] at hrs hpr' hqt'
   rw [le_abs] at hst ⊢
   cases hst

Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

@@ -147,7 +147,7 @@ theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card)
         rw [coe_energy, add_div, mul_div_cancel_left]; positivity
     _ ≤ (∑ x in P.parts.offDiag.attach, (∑ i in distinctPairs G ε hP x,
           G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card) / P.parts.card ^ 2 :=
-        div_le_div_of_le_of_nonneg ?_ $ by positivity
+        div_le_div_of_le (by positivity) ?_
     _ = (∑ x in P.parts.offDiag.attach, ∑ i in distinctPairs G ε hP x,
           G.edgeDensity i.1 i.2 ^ 2 : ℝ) / (increment hP G ε).parts.card ^ 2 := by
         rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -802,7 +802,7 @@ theorem tendsto_translation_number' (x : ℝ) :
 
 theorem translationNumber_mono : Monotone τ := fun f g h =>
   le_of_tendsto_of_tendsto' f.tendsto_translation_number₀ g.tendsto_translation_number₀ fun n =>
-    div_le_div_of_le_of_nonneg (pow_mono h n 0) n.cast_nonneg
+    div_le_div_of_le n.cast_nonneg (pow_mono h n 0)
 #align circle_deg1_lift.translation_number_mono CircleDeg1Lift.translationNumber_mono
 
 theorem translationNumber_translate (x : ℝ) : τ (translate <| Multiplicative.ofAdd x) = x :=

Mathlib/Topology/UrysohnsLemma.lean

@@ -301,8 +301,8 @@ theorem continuous_lim (c : CU P) : Continuous c.lim := by
       simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint,
         c.left.left.lim_of_nmem_U _ hxl, c.left.left.lim_of_nmem_U _ hyl]
       refine' (dist_midpoint_midpoint_le _ _ _ _).trans _
-      refine' (div_le_div_of_le_of_nonneg (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _)
-        zero_le_two).trans _
+      refine' (div_le_div_of_le zero_le_two
+        (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _)).trans _
       rw [dist_self, zero_add]
       set r := (3 / 4 : ℝ) ^ n
       calc _ ≤ (r / 2 + r) / 2 := by gcongr