chore: assorted golf (#19319)

Archive/Imo/Imo2008Q2.lean

@@ -106,12 +106,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
             exact ⟨rfl, rfl, rfl⟩
         · have hg : -z = g (x, y, z) := rfl
           rw [hg, hz_def]; ring
-      have h₂ : q < t * (t + 1) := by
-        calc
-          q < q + 1 := by linarith
-          _ ≤ t := le_max_left (q + 1) 1
-          _ ≤ t + t ^ 2 := by linarith [sq_nonneg t]
-          _ = t * (t + 1) := by ring
+      have h₂ : q < t * (t + 1) := by linarith [sq_nonneg t, le_max_left (q + 1) 1]
       exact ⟨h₁, h₂⟩
     have hK_inf : Set.Infinite K := by intro h; apply hK_not_bdd; exact Set.Finite.bddAbove h
     exact hK_inf.of_image g

Archive/Imo/Imo2013Q5.lean

@@ -65,15 +65,9 @@ theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
   refine le_of_all_pow_lt_succ hx ?_ h
   by_contra! hy'' : y ≤ 1
   -- Then there exists y' such that 0 < y ≤ 1 < y' < x.
-  let y' := (x + 1) / 2
-  have h_y'_lt_x : y' < x :=
-    calc
-      (x + 1) / 2 < x * 2 / 2 := by linarith
-      _ = x := by field_simp
-  have h1_lt_y' : 1 < y' :=
-    calc
-      1 = 1 * 2 / 2 := by field_simp
-      _ < (x + 1) / 2 := by linarith
+  have h_y'_lt_x : (x + 1) / 2 < x := by linarith
+  have h1_lt_y' : 1 < (x + 1) / 2 := by linarith
+  set y' := (x + 1) / 2
   have h_y_lt_y' : y < y' := by linarith
   have hh : ∀ n, 0 < n → x ^ n - 1 < y' ^ n := by
     intro n hn

Mathlib/Analysis/Calculus/Monotone.lean

@@ -108,7 +108,7 @@ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
       filter_upwards [this]
       rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
       rw [mem_Iio]
-      norm_num; nlinarith
+      nlinarith
   -- Deduce the correct limit on the left, by sandwiching.
   have L4 :
     Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv f.measure volume x).toReal) := by
@@ -118,7 +118,7 @@ theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
       refine div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 ?_)
       apply f.mono.le_leftLim
       have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
-      norm_num; linarith
+      linarith
     · filter_upwards [self_mem_nhdsWithin]
       rintro y (hy : y < x)
       refine div_le_div_of_nonpos_of_le (by linarith) ?_
@@ -161,7 +161,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
         filter_upwards [this]
         rintro y ⟨hy : x < y, h'y : y < x + 1⟩
         rw [mem_Ioi]
-        norm_num; nlinarith
+        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] with y hy
@@ -190,7 +190,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
         rintro y hy
         rw [mem_Ioo] at hy
         rw [mem_Iio]
-        norm_num; nlinarith
+        nlinarith
     -- apply the sandwiching argument, with `g` and the helper function
     apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
     · filter_upwards [self_mem_nhdsWithin]
@@ -203,7 +203,7 @@ theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
       rw [mem_Iio, ← sub_neg] at hy
       have : 0 < (y - x) ^ 2 := sq_pos_of_neg hy
       apply div_le_div_of_nonpos_of_le hy.le
-      exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
+      exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by linarith))
   -- conclude global differentiability
   rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, (nhds_left'_sup_nhds_right' x).symm,
     tendsto_sup]

Mathlib/Analysis/Convex/Uniform.lean

@@ -96,16 +96,7 @@ theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
     _ ≤ 2 - δ + δ' + δ' :=
       (add_le_add_three (h (h₁ _ hx') (h₁ _ hy') hxy') (h₂ _ hx hx'.le) (h₂ _ hy hy'.le))
     _ ≤ 2 - δ' := by
-      dsimp only [δ']
-      rw [← le_sub_iff_add_le, ← le_sub_iff_add_le, sub_sub, sub_sub]
-      refine sub_le_sub_left ?_ _
-      ring_nf
-      rw [← mul_div_cancel₀ δ three_ne_zero]
-      norm_num
-      -- Porting note: these three extra lines needed to make `exact` work
-      have : 3 * (δ / 3) * (1 / 3) = δ / 3 := by linarith
-      rw [this, mul_comm]
-      gcongr
+      suffices δ' ≤ δ / 3 by linarith
       exact min_le_of_right_le <| min_le_right _ _
 
 theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :

Mathlib/Analysis/PSeries.lean

@@ -386,12 +386,9 @@ theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) :
   simp only [sub_eq_add_neg, add_assoc, Nat.cast_add, Nat.cast_one, le_add_neg_iff_add_le,
     add_le_iff_nonpos_right, neg_add_le_iff_le_add, add_zero]
   have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
-  have B : 0 < (n : α) + 1 := by linarith
   field_simp
-  rw [div_le_div_iff₀ _ A, ← sub_nonneg]
-  · ring_nf
-    rw [add_comm]
-    exact B.le
+  rw [div_le_div_iff₀ _ A]
+  · linarith
   · -- Porting note: was `nlinarith`
     positivity
 

Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

@@ -57,7 +57,7 @@ theorem Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : ℝ} (hs : 0 <
   let f : ℝ → ℝ → ℝ → ℝ := fun c u x => exp (-c * x) * x ^ (c * (u - 1))
   have e : IsConjExponent (1 / a) (1 / b) := Real.isConjExponent_one_div ha hb hab
   have hab' : b = 1 - a := by linarith
-  have hst : 0 < a * s + b * t := add_pos (mul_pos ha hs) (mul_pos hb ht)
+  have hst : 0 < a * s + b * t := by positivity
   -- some properties of f:
   have posf : ∀ c u x : ℝ, x ∈ Ioi (0 : ℝ) → 0 ≤ f c u x := fun c u x hx =>
     mul_nonneg (exp_pos _).le (rpow_pos_of_pos hx _).le

Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

@@ -53,26 +53,24 @@ theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
   intro x hex y _ hxy
   have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
   have y_pos : 0 < y := by linarith
-  have x_nonneg : 0 ≤ x := le_trans (le_of_lt (exp_pos (1 / a))) hex
-  have y_nonneg : 0 ≤ y := by linarith
   nth_rw 1 [← rpow_one y]
   nth_rw 1 [← rpow_one x]
-  rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_nonneg, rpow_mul x_nonneg,
+  rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_pos.le, rpow_mul x_pos.le,
     log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
     mul_div_assoc, mul_le_mul_left (one_div_pos.mpr ha)]
   refine log_div_self_antitoneOn ?_ ?_ ?_
   · simp only [Set.mem_setOf_eq]
     convert rpow_le_rpow _ hex (le_of_lt ha) using 1
     · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
-      field_simp [(ne_of_lt ha).symm]
-    exact le_of_lt (exp_pos (1 / a))
+      field_simp
+    positivity
   · simp only [Set.mem_setOf_eq]
     convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
     · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
-      field_simp [(ne_of_lt ha).symm]
-    exact le_of_lt (exp_pos (1 / a))
+      field_simp
+    positivity
   gcongr
 
 theorem log_div_sqrt_antitoneOn : AntitoneOn (fun x : ℝ => log x / √x) { x | exp 2 ≤ x } := by

Mathlib/NumberTheory/FermatPsp.lean

@@ -197,10 +197,8 @@ private theorem psp_from_prime_psp {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_p
   have hi_p : 1 ≤ p := Nat.one_le_of_lt p_gt_two
   have hi_bsquared : 0 < b ^ 2 - 1 := by
     -- Porting note: was `by nlinarith [Nat.one_le_pow 2 b hi_b]`
-    have h0 := mul_le_mul b_ge_two b_ge_two zero_le_two hi_b.le
-    have h1 : 1 < 2 * 2 := by omega
-    have := tsub_pos_of_lt (h1.trans_le h0)
-    rwa [pow_two]
+    have := Nat.pow_le_pow_left b_ge_two 2
+    omega
   have hi_bpowtwop : 1 ≤ b ^ (2 * p) := Nat.one_le_pow (2 * p) b hi_b
   have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_b
   -- Other useful facts

Mathlib/NumberTheory/Modular.lean

@@ -458,11 +458,8 @@ theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |g 1 0| 
       specialize this hc
       linarith
   intro hc
-  replace hc : 0 < c ^ 4 := by
-    change 0 < c ^ (2 * 2); rw [pow_mul]; apply sq_pos_of_pos (sq_pos_of_ne_zero hc)
-  have h₁ := mul_lt_mul_of_pos_right
-      (mul_lt_mul'' (three_lt_four_mul_im_sq_of_mem_fdo hg) (three_lt_four_mul_im_sq_of_mem_fdo hz)
-      (by norm_num) (by norm_num)) hc
+  have h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
+    gcongr <;> apply three_lt_four_mul_im_sq_of_mem_fdo <;> assumption
   have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
     div_le_one_of_le₀
       (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g))

Mathlib/Topology/MetricSpace/Kuratowski.lean

@@ -68,8 +68,7 @@ theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSub
         apply_rules [add_le_add_left, le_abs_self]
       _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
         rw [C]
-        apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
-        norm_num
+        gcongr
       _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
         have : |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤
             dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by