chore: lighten tactics (#19318)

Change some tactic uses to more lightweight ones (but which still automate just as much): `nlinarith` to `positivity`/`linarith`/`gcongr`, `linarith` to `norm_num`.
leanprover-community · Nov 21, 2024 · 06553ac · 06553ac
1 parent d1c99f2
commit 06553ac
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 16 deletions.
diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean
@@ -1504,7 +1504,7 @@ theorem abs_sub_round_div_natCast_eq {m n : ℕ} :
 
 @[bound]
 theorem sub_half_lt_round (x : α) : x - 1 / 2 < round x := by
-  rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by nlinarith]
+  rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]
   exact Int.sub_one_lt_floor (x + 1 / 2)
 
 @[bound]

diff --git a/Mathlib/Analysis/Convex/Slope.lean b/Mathlib/Analysis/Convex/Slope.lean
@@ -40,7 +40,7 @@ theorem ConvexOn.slope_mono_adjacent (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx
   field_simp [a, b, mul_comm (z - x) _] at key ⊢
   rw [div_le_div_iff_of_pos_right]
   · linarith
-  · nlinarith
+  · positivity
 
 /-- If `f : 𝕜 → 𝕜` is concave, then for any three points `x < y < z` the slope of the secant line of
 `f` on `[x, y]` is greater than the slope of the secant line of `f` on `[y, z]`. -/
@@ -73,7 +73,7 @@ theorem StrictConvexOn.slope_strict_mono_adjacent (hf : StrictConvexOn 𝕜 s f)
   field_simp [mul_comm (z - x) _] at key ⊢
   rw [div_lt_div_iff_of_pos_right]
   · linarith
-  · nlinarith
+  · positivity
 
 /-- If `f : 𝕜 → 𝕜` is strictly concave, then for any three points `x < y < z` the slope of the
 secant line of `f` on `[x, y]` is strictly greater than the slope of the secant line of `f` on

diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
@@ -389,8 +389,7 @@ theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) :
   field_simp
   rw [div_le_div_iff₀ _ A]
   · linarith
-  · -- Porting note: was `nlinarith`
-    positivity
+  · positivity
 
 theorem sum_Ioo_inv_sq_le (k n : ℕ) : (∑ i ∈ Ioo k n, (i ^ 2 : α)⁻¹) ≤ 2 / (k + 1) :=
   calc

diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
@@ -589,7 +589,7 @@ open Real Filter
 theorem tendsto_one_plus_div_rpow_exp (t : ℝ) :
     Tendsto (fun x : ℝ => (1 + t / x) ^ x) atTop (𝓝 (exp t)) := by
   apply ((Real.continuous_exp.tendsto _).comp (tendsto_mul_log_one_plus_div_atTop t)).congr' _
-  have h₁ : (1 : ℝ) / 2 < 1 := by linarith
+  have h₁ : (1 : ℝ) / 2 < 1 := by norm_num
   have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by
     simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
   refine (eventually_ge_of_tendsto_gt h₁ h₂).mono fun x hx => ?_

diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean
@@ -304,7 +304,7 @@ private theorem psp_from_prime_gt_p {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_
   suffices h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2 by
     apply gt_of_ge_of_gt
     · exact tsub_le_tsub_left (one_le_of_lt p_gt_two) ((b ^ 2) ^ (p - 1) * b ^ 2)
-    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right _ (show 0 < b ^ 2 by nlinarith)
+    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right _ (show 0 < b ^ 2 by positivity)
       exact tsub_lt_tsub_right_of_le this h
   suffices h : p < (b ^ 2) ^ (p - 1) by
     have : 4 ≤ b ^ 2 := by nlinarith

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -441,9 +441,7 @@ lemma sup_pow_add_le_pow_sup_pow {n m : ℕ} : (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔
       ((Ideal.pow_le_pow_right hn).trans le_sup_left)))
   · refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans
       ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))
-    simp only [Finset.mem_range, Nat.lt_succ] at hi
-    rw [Nat.le_sub_iff_add_le hi]
-    nlinarith
+    omega
 
 variable (I J K)
 

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -70,12 +70,10 @@ theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSub
         rw [C]
         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
-          simp only [dist_eq_norm]
-          exact lp.norm_apply_le_norm ENNReal.top_ne_zero
-            (embeddingOfSubset x b - embeddingOfSubset x a) n
-        nlinarith
+        gcongr
+        simp only [dist_eq_norm]
+        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
+          (embeddingOfSubset x b - embeddingOfSubset x a) n
       _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
   simpa [dist_comm] using this