chore: Rename monotonicity of / lemmas (#10634)

The new names and argument orders match the corresponding `*` lemmas, which I already took care of in a previous PR.

From LeanAPAP

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -514,7 +514,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
         positivity
       rw [abs_of_pos this]
     rwa [this]
-  suffices 0 < denom ∧ denom ≤ denom' from div_le_div_of_le_left zero_le_one this.left this.right
+  suffices 0 < denom ∧ denom ≤ denom' from div_le_div_of_nonneg_left zero_le_one this.1 this.2
   constructor
   · have : 0 < pred_conts.b + gp.b * conts.b :=
       nextConts_b_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _

Mathlib/Algebra/Order/Field/Basic.lean

@@ -347,31 +347,43 @@ theorem one_le_inv_iff : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 :=
 
 
 @[mono, gcongr]
-theorem div_le_div_of_le (hc : 0 ≤ c) (h : a ≤ b) : a / c ≤ b / c := by
+lemma div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c := by
   rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 hc)
-#align div_le_div_of_le div_le_div_of_le
+  exact mul_le_mul_of_nonneg_right hab (one_div_nonneg.2 hc)
+#align div_le_div_of_le_of_nonneg div_le_div_of_nonneg_right
+
+@[gcongr]
+lemma div_lt_div_of_pos_right (h : a < b) (hc : 0 < c) : a / c < b / c := by
+  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
+  exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)
+#align div_lt_div_of_lt div_lt_div_of_pos_right
 
 -- Not a `mono` lemma b/c `div_le_div` is strictly more general
 @[gcongr]
-theorem div_le_div_of_le_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c := by
+lemma div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c := by
   rw [div_eq_mul_inv, div_eq_mul_inv]
   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
+#align div_le_div_of_le_left div_le_div_of_nonneg_left
 
 @[gcongr]
-theorem div_lt_div_of_lt (hc : 0 < c) (h : a < b) : a / c < b / c := by
-  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
-  exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)
-#align div_lt_div_of_lt div_lt_div_of_lt
+lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c := by
+  simpa only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv (hc.trans h) hc]
+#align div_lt_div_of_lt_left div_lt_div_of_pos_left
+
+-- 2024-02-16
+@[deprecated] alias div_le_div_of_le_of_nonneg := div_le_div_of_nonneg_right
+@[deprecated] alias div_lt_div_of_lt := div_lt_div_of_pos_right
+@[deprecated] alias div_le_div_of_le_left := div_le_div_of_nonneg_left
+@[deprecated] alias div_lt_div_of_lt_left := div_lt_div_of_pos_left
+
+@[deprecated div_le_div_of_nonneg_right]
+lemma div_le_div_of_le (hc : 0 ≤ c) (hab : a ≤ b) : a / c ≤ b / c :=
+  div_le_div_of_nonneg_right hab hc
+#align div_le_div_of_le div_le_div_of_le
 
 theorem div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b :=
-  ⟨le_imp_le_of_lt_imp_lt <| div_lt_div_of_lt hc, div_le_div_of_le <| hc.le⟩
+  ⟨le_imp_le_of_lt_imp_lt fun hab ↦ div_lt_div_of_pos_right hab hc,
+    fun hab ↦ div_le_div_of_nonneg_right hab hc.le⟩
 #align div_le_div_right div_le_div_right
 
 theorem div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b :=
@@ -409,26 +421,21 @@ theorem div_lt_div' (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) : a
   (div_lt_div_iff (d0.trans hbd) d0).2 (mul_lt_mul' hac hbd d0.le c0)
 #align div_lt_div' div_lt_div'
 
-@[gcongr]
-theorem div_lt_div_of_lt_left (hc : 0 < c) (hb : 0 < b) (h : b < a) : c / a < c / b :=
-  (div_lt_div_left hc (hb.trans h) hb).mpr h
-#align div_lt_div_of_lt_left div_lt_div_of_lt_left
-
 /-!
 ### Relating one division and involving `1`
 -/
 
 
 theorem div_le_self (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a := by
-  simpa only [div_one] using div_le_div_of_le_left ha zero_lt_one hb
+  simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb
 #align div_le_self div_le_self
 
 theorem div_lt_self (ha : 0 < a) (hb : 1 < b) : a / b < a := by
-  simpa only [div_one] using div_lt_div_of_lt_left ha zero_lt_one hb
+  simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb
 #align div_lt_self div_lt_self
 
 theorem le_div_self (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b := by
-  simpa only [div_one] using div_le_div_of_le_left ha hb₀ hb₁
+  simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁
 #align le_div_self le_div_self
 
 theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff hb, one_mul]
@@ -562,6 +569,11 @@ theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by
 ### Miscellaneous lemmas
 -/
 
+@[simp] lemma div_pos_iff_of_pos_left (ha : 0 < a) : 0 < a / b ↔ 0 < b := by
+  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]
+
+@[simp] lemma div_pos_iff_of_pos_right (hb : 0 < b) : 0 < a / b ↔ 0 < a := by
+  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]
 
 theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c := by
   rw [← mul_div_assoc] at h
@@ -586,10 +598,14 @@ theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧
   ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩
 #align exists_pos_lt_mul exists_pos_lt_mul
 
+lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) :=
+  fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha
+
+lemma strictMono_div_right_of_pos (ha : 0 < a) : StrictMono (· / a) :=
+  fun _b _c hbc ↦ div_lt_div_of_pos_right hbc ha
+
 theorem Monotone.div_const {β : Type*} [Preorder β] {f : β → α} (hf : Monotone f) {c : α}
-    (hc : 0 ≤ c) : Monotone fun x => f x / c := by
-  haveI := @LinearOrder.decidableLE α _
-  simpa only [div_eq_mul_inv] using (monotone_mul_right_of_nonneg (inv_nonneg.2 hc)).comp hf
+    (hc : 0 ≤ c) : Monotone fun x => f x / c := (monotone_div_right_of_nonneg hc).comp hf
 #align monotone.div_const Monotone.div_const
 
 theorem StrictMono.div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α}
@@ -603,20 +619,20 @@ instance (priority := 100) LinearOrderedSemiField.toDenselyOrdered : DenselyOrde
     ⟨(a₁ + a₂) / 2,
       calc
         a₁ = (a₁ + a₁) / 2 := (add_self_div_two a₁).symm
-        _ < (a₁ + a₂) / 2 := div_lt_div_of_lt zero_lt_two (add_lt_add_left h _)
+        _ < (a₁ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_left h _) zero_lt_two
         ,
       calc
-        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_lt zero_lt_two (add_lt_add_right h _)
+        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_right h _) zero_lt_two
         _ = a₂ := add_self_div_two a₂
         ⟩
 #align linear_ordered_field.to_densely_ordered LinearOrderedSemiField.toDenselyOrdered
 
 theorem min_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = min a b / c :=
-  Eq.symm <| Monotone.map_min fun _ _ => div_le_div_of_le hc
+  (monotone_div_right_of_nonneg hc).map_min.symm
 #align min_div_div_right min_div_div_right
 
 theorem max_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : max (a / c) (b / c) = max a b / c :=
-  Eq.symm <| Monotone.map_max fun _ _ => div_le_div_of_le hc
+  (monotone_div_right_of_nonneg hc).map_max.symm
 #align max_div_div_right max_div_div_right
 
 theorem one_div_strictAntiOn : StrictAntiOn (fun x : α => 1 / x) (Set.Ioi 0) :=

Mathlib/Algebra/Order/Field/Power.lean

@@ -237,7 +237,7 @@ theorem Nat.cast_le_pow_sub_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ (a ^ n
 `Nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
 theorem Nat.cast_le_pow_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a - 1) :=
   (n.cast_le_pow_sub_div_sub H).trans <|
-    div_le_div_of_le (sub_nonneg.2 H.le) (sub_le_self _ zero_le_one)
+    div_le_div_of_nonneg_right (sub_le_self _ zero_le_one) (sub_nonneg.2 H.le)
 #align nat.cast_le_pow_div_sub Nat.cast_le_pow_div_sub
 
 end LinearOrderedField

Mathlib/Algebra/Order/Floor.lean

@@ -542,7 +542,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 n.cast_nonneg (floor_le ha))
+  · exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg)
   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/Complex/UpperHalfPlane/Metric.lean

@@ -245,9 +245,11 @@ theorem dist_log_im_le (z w : ℍ) : dist (log z.im) (log w.im) ≤ dist z w :=
   calc
     dist (log z.im) (log w.im) = dist (mk ⟨0, z.im⟩ z.im_pos) (mk ⟨0, w.im⟩ w.im_pos) :=
       Eq.symm <| dist_of_re_eq rfl
-    _ ≤ dist z w := mul_le_mul_of_nonneg_left (arsinh_le_arsinh.2 <|
-      div_le_div_of_le (mul_nonneg zero_le_two (sqrt_nonneg _)) <| by
-        simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_abs (z - w)) zero_le_two
+    _ ≤ dist z w := by
+      simp_rw [dist_eq]
+      gcongr
+      · simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_abs (z - w)
+      · simp
 #align upper_half_plane.dist_log_im_le UpperHalfPlane.dist_log_im_le
 
 theorem im_le_im_mul_exp_dist (z w : ℍ) : z.im ≤ w.im * Real.exp (dist z w) := by

Mathlib/Analysis/Convex/Strong.lean

@@ -127,11 +127,10 @@ def StrongConcaveOn (s : Set E) (m : ℝ) : (E → ℝ) → Prop :=
 variable {s : Set E} {f : E → ℝ} {m n : ℝ}
 
 nonrec lemma StrongConvexOn.mono (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f :=
-  hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) <| by positivity
+  hf.mono fun r ↦ by gcongr
 
 nonrec lemma StrongConcaveOn.mono (hmn : m ≤ n) (hf : StrongConcaveOn s n f) :
-    StrongConcaveOn s m f :=
-  hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) <| by positivity
+    StrongConcaveOn s m f := hf.mono fun r ↦ by gcongr
 
 @[simp] lemma strongConvexOn_zero : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f := by
   simp [StrongConvexOn, ← Pi.zero_def]

Mathlib/Analysis/Normed/Group/ControlledClosure.lean

@@ -44,11 +44,7 @@ theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgr
     of a sequence `v` of elements of `K` which starts close to `h` and then quickly goes to zero.
     The sequence `b` below quantifies this. -/
   set b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
-  have b_pos : ∀ i, 0 < b i := by
-    intro i
-    field_simp [b, hC]
-    exact
-      div_pos (mul_pos hε (norm_pos_iff.mpr hyp_h)) (mul_pos (by norm_num : (0 : ℝ) < 2 ^ i * 2) hC)
+  have b_pos (i) : 0 < b i := by field_simp [b, hC, hyp_h]
   obtain
     ⟨v : ℕ → H, lim_v : Tendsto (fun n : ℕ => ∑ k in range (n + 1), v k) atTop (𝓝 h), v_in :
       ∀ n, v n ∈ K, hv₀ : ‖v 0 - h‖ < b 0, hv : ∀ n > 0, ‖v n‖ < b n⟩ :=

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 (norm_nonneg _) (norm_add_le _ _)
+  exact div_le_div_of_nonneg_right (norm_add_le _ _) (norm_nonneg _)
 #align dist_midpoint_midpoint_le' dist_midpoint_midpoint_le'
 
 theorem nndist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :

Mathlib/Analysis/SpecialFunctions/Arsinh.lean

@@ -148,6 +148,8 @@ theorem arsinh_le_arsinh : arsinh x ≤ arsinh y ↔ x ≤ y :=
   sinhOrderIso.symm.le_iff_le
 #align real.arsinh_le_arsinh Real.arsinh_le_arsinh
 
+@[gcongr] protected alias ⟨_, GCongr.arsinh_le_arsinh⟩ := arsinh_le_arsinh
+
 @[simp]
 theorem arsinh_lt_arsinh : arsinh x < arsinh y ↔ x < y :=
   sinhOrderIso.symm.lt_iff_lt

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -235,9 +235,7 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a
   calc
     x ^ n ≤ ⌈x⌉₊ ^ n := mod_cast pow_le_pow_left hx₀.le (Nat.le_ceil _) _
     _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
-    _ ≤ exp (x + 1) / (exp 1 * C) :=
-      (div_le_div_of_le (mul_pos (exp_pos _) hC₀).le
-        (exp_le_exp.2 <| (Nat.ceil_lt_add_one hx₀.le).le))
+    _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
     _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
 #align real.tendsto_exp_div_pow_at_top Real.tendsto_exp_div_pow_atTop
 

Mathlib/Analysis/Subadditive.lean

@@ -78,7 +78,7 @@ theorem eventually_div_lt_of_div_lt {L : ℝ} {n : ℕ} (hn : n ≠ 0) (hL : u n
   rw [mul_comm]
   refine lt_of_le_of_lt ?_ hk
   simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
-  exact div_le_div_of_le (Nat.cast_nonneg _) (h.apply_mul_add_le _ _ _)
+  exact div_le_div_of_nonneg_right (h.apply_mul_add_le _ _ _) (Nat.cast_nonneg _)
 #align subadditive.eventually_div_lt_of_div_lt Subadditive.eventually_div_lt_of_div_lt
 
 /-- Fekete's lemma: a subadditive sequence which is bounded below converges. -/

Mathlib/Combinatorics/Additive/Behrend.lean

@@ -256,7 +256,7 @@ theorem exists_large_sphere (n d : ℕ) :
   · simp
   obtain rfl | hd := d.eq_zero_or_pos
   · simp
-  refine' (div_le_div_of_le_left _ _ _).trans hk
+  refine' (div_le_div_of_nonneg_left _ _ _).trans hk
   · exact cast_nonneg _
   · exact cast_add_one_pos _
   simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow,
@@ -327,13 +327,11 @@ theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) 
 
 theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x⌉₊) / ⌈x⌉₊ := by
   have h₁ := ceil_lt_add_one hx.le
-  have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by
-    rw [_root_.le_sub_iff_add_le]
-    apply (add_le_add_left h₁.le _).trans_eq
-    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 (add_nonneg hx.le zero_le_one) (exp_le_exp.2 h₂))
+  have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith
+  calc
+    _ ≤ exp (1 - x) / (x + 1) := ?_
+    _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
+    _ < _ := by gcongr
   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 _)
@@ -429,7 +427,7 @@ set_option linter.uppercaseLean3 false in
 theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dValue N := by
   apply div_lt_floor _
   rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv]
-  · apply le_trans _ (div_le_div_of_le_left _ _ (ceil_lt_mul _).le)
+  · apply le_trans _ (div_le_div_of_nonneg_left _ _ (ceil_lt_mul _).le)
     rw [mul_comm, ← div_div, div_sqrt, le_div_iff]
     · set_option tactic.skipAssignedInstances false in norm_num; exact le_sqrt_log hN
     · norm_num1

Mathlib/Combinatorics/Schnirelmann.lean

@@ -93,7 +93,7 @@ lemma schnirelmannDensity_le_of_not_mem {k : ℕ} (hk : k ∉ A) :
   · simpa using schnirelmannDensity_le_one
   apply schnirelmannDensity_le_of_le k hk'.ne'
   rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']
-  apply div_le_div_of_le (Nat.cast_nonneg _)
+  gcongr
   rw [← Nat.cast_pred hk', Nat.cast_le]
   suffices (Ioc 0 k).filter (· ∈ A) ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
   rw [← Ioo_insert_right hk', filter_insert, if_neg hk]
@@ -106,8 +106,8 @@ lemma schnirelmannDensity_eq_zero_of_one_not_mem (h : 1 ∉ A) : schnirelmannDen
 /-- The Schnirelmann density is increasing with the set. -/
 lemma schnirelmannDensity_le_of_subset {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A ⊆ B) :
     schnirelmannDensity A ≤ schnirelmannDensity B :=
-  ciInf_mono ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩ fun _ => div_le_div_of_le (by positivity) <|
-    Nat.cast_le.2 <| card_le_card <| monotone_filter_right _ h
+  ciInf_mono ⟨0, fun _ ⟨_, hx⟩ ↦ hx ▸ by positivity⟩ fun _ ↦ by
+    gcongr; exact monotone_filter_right _ h
 
 /-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/
 lemma schnirelmannDensity_eq_one_iff : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A := by
@@ -196,8 +196,7 @@ lemma schnirelmannDensity_finset (A : Finset ℕ) : schnirelmannDensity A = 0 :=
   have hn : 0 < n := Nat.succ_pos _
   use n, hn
   rw [div_lt_iff (Nat.cast_pos.2 hn), ← div_lt_iff' hε, Nat.cast_add_one]
-  exact (Nat.lt_floor_add_one _).trans_le' <| div_le_div_of_le hε.le <| Nat.cast_le.2 <|
-    card_le_card <| by simp [subset_iff]
+  exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff]
 
 /-- The Schnirelmann density of any finite set is `0`. -/
 lemma schnirelmannDensity_finite {A : Set ℕ} [DecidablePred (· ∈ A)] (hA : A.Finite) :

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -240,7 +240,7 @@ theorem IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)}
     rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
     refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
     rw [mem_range] at hr
-    refine' div_le_div_of_le_left _ _ _ <;> norm_cast
+    refine' div_le_div_of_nonneg_left _ _ _ <;> norm_cast
     · exact Nat.zero_le _
     · exact choose_pos (Nat.lt_succ_iff.1 hr)
     · exact choose_le_middle _ _

Mathlib/Combinatorics/SimpleGraph/Density.lean

@@ -186,8 +186,8 @@ theorem mul_edgeDensity_le_edgeDensity (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁)
     (s₂.card : ℚ) / s₁.card * (t₂.card / t₁.card) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁ := by
   have hst : (s₂.card : ℚ) * t₂.card ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
   rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel _ hst]
-  refine' div_le_div_of_le (mod_cast (s₁.card * t₁.card).zero_le) _
-  exact mod_cast card_le_card (interedges_mono hs ht)
+  gcongr
+  exact interedges_mono hs ht
 #align rel.mul_edge_density_le_edge_density Rel.mul_edgeDensity_le_edgeDensity
 
 theorem edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty)