chore(*): minor golfs, mostly using gcongr (#9577)

Mathlib/Analysis/Calculus/Monotone.lean

@@ -168,15 +168,14 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
         norm_num; nlinarith
     -- apply the sandwiching argument, with the helper function and `g`
     apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
-    · 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 (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 (sub_pos.2 hy).le
-      exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl y))
+    · filter_upwards [self_mem_nhdsWithin] with y (hy : x < y)
+      rw [← sub_pos] at hy
+      gcongr
+      exact hf.rightLim_le (by nlinarith)
+    · filter_upwards [self_mem_nhdsWithin] with y (hy : x < y)
+      rw [← sub_pos] at hy
+      gcongr
+      exact hf.le_rightLim le_rfl
   -- prove differentiability on the left, by sandwiching with values of `g`
   have L2 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x)
       (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by

Mathlib/Combinatorics/Schnirelmann.lean

@@ -223,9 +223,9 @@ lemma schnirelmannDensity_setOf_mod_eq_one {m : ℕ} (hm : m ≠ 1) :
     refine schnirelmannDensity_finite ?_
     simp
   apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _
-  · rw [← one_div]
-    apply div_le_div_of_le (Nat.cast_nonneg _)
-    simp only [Set.mem_setOf_eq, Nat.cast_le_one, card_le_one_iff_subset_singleton, subset_iff,
+  · rw [← one_div, ← @Nat.cast_one ℝ]
+    gcongr
+    simp only [Set.mem_setOf_eq, card_le_one_iff_subset_singleton, subset_iff,
       mem_filter, mem_Ioc, mem_singleton, and_imp]
     use 1
     intro x _ hxm h

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -130,11 +130,10 @@ theorem eps_pos (hPε : 100 ≤ (4 : ℝ) ^ P.parts.card * ε ^ 5) : 0 < ε :=
 
 theorem hundred_div_ε_pow_five_le_m [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α)
     (hPε : 100 ≤ (4 : ℝ) ^ P.parts.card * ε ^ 5) : 100 / ε ^ 5 ≤ m :=
-  (div_le_of_nonneg_of_le_mul (eps_pow_five_pos hPε).le (by positivity) hPε).trans
-    (by
-      norm_cast
-      rwa [Nat.le_div_iff_mul_le' (stepBound_pos (P.parts_nonempty <|
-        univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow])
+  (div_le_of_nonneg_of_le_mul (eps_pow_five_pos hPε).le (by positivity) hPε).trans <| by
+    norm_cast
+    rwa [Nat.le_div_iff_mul_le' (stepBound_pos (P.parts_nonempty <|
+      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]
 #align szemeredi_regularity.hundred_div_ε_pow_five_le_m SzemerediRegularity.hundred_div_ε_pow_five_le_m
 
 theorem hundred_le_m [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α)

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -342,7 +342,7 @@ private theorem average_density_near_total_density [Nonempty α]
   suffices (G.edgeDensity (A.biUnion id) (B.biUnion id) : ℝ) -
       (∑ ab in A.product B, (G.edgeDensity ab.1 ab.2 : ℝ)) / (A.card * B.card) ≤ ε ^ 5 / 50 by
     apply this.trans
-    exact div_le_div_of_le_left (by sz_positivity) (by norm_num) (by norm_num)
+    gcongr <;> [sz_positivity; norm_num]
   rw [sub_le_iff_le_add, ← sub_le_iff_le_add']
   apply density_sub_eps_le_sum_density_div_card hPα hPε hA hB
 

Mathlib/NumberTheory/NumberField/Discriminant.lean

@@ -166,10 +166,9 @@ theorem abs_discr_ge (h : 1 < finrank ℚ K) :
   let a : ℕ → ℝ := fun n => (n:ℝ) ^ (n * 2) / ((4 / π) ^ n * (n.factorial:ℝ) ^ 2)
   suffices ∀ n, 2 ≤ n → (4 / 9 : ℝ) * (3 * π / 4) ^ n ≤ a n by
     refine le_trans (this (finrank ℚ K) h) ?_
-    refine div_le_div_of_le_left (by positivity) (by positivity) ?_
-    refine mul_le_mul_of_nonneg_right (pow_le_pow_right ?_ ?_) (by positivity)
-    · rw [_root_.le_div_iff Real.pi_pos, one_mul]
-      exact Real.pi_le_four
+    simp only -- unfold `a` and beta-reduce
+    gcongr
+    · exact (one_le_div Real.pi_pos).2 Real.pi_le_four
     · rw [← card_add_two_mul_card_eq_rank, mul_comm]
       exact Nat.le_add_left _ _
   intro n hn