diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index d3d6e7b16dc1d..0ec2dc284de96 100644 --- 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 index 1ecc6866a18aa..51a20a60734cd 100644 --- 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 index 93a65386cf5e2..38fe34d857d76 100644 --- 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 index d05eed644c71c..71ae3fbd4d054 100644 --- 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 index b5c6b98a175d6..31cdde409beb6 100644 --- 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 index e18052a266b00..13dfba254995d 100644 --- 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 index 7b7e6e47ae7f0..a0fa5566df6e3 100644 --- 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