diff --git a/Archive/Imo/Imo2005Q3.lean b/Archive/Imo/Imo2005Q3.lean index 5048b0487e381..fd86a1a27cdfd 100644 --- a/Archive/Imo/Imo2005Q3.lean +++ b/Archive/Imo/Imo2005Q3.lean @@ -25,9 +25,6 @@ namespace Imo2005Q3 theorem key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) : (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) := by - have h₁ : x ^ 5 + y ^ 2 + z ^ 2 ≠ 0 := by positivity - have h₃ : x ^ 2 + y ^ 2 + z ^ 2 ≠ 0 := by positivity - have h₄ : x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2) ≠ 0 := by positivity have key : (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) = diff --git a/Archive/Imo/Imo2008Q2.lean b/Archive/Imo/Imo2008Q2.lean index ab0b7cfc99eb0..00885102e38bf 100644 --- a/Archive/Imo/Imo2008Q2.lean +++ b/Archive/Imo/Imo2008Q2.lean @@ -68,10 +68,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by simp only [Set.mem_setOf_eq] at hs_in_W ⊢ rcases hs_in_W with ⟨x, y, z, h₁, t, ht_gt_zero, hx_t, hy_t, hz_t⟩ use x, y, z - have ht_ne_zero : t ≠ 0 := ne_of_gt ht_gt_zero - have ht1_ne_zero : t + 1 ≠ 0; linarith [ht_gt_zero] have key_gt_zero : t ^ 2 + t + 1 > 0; linarith [pow_pos ht_gt_zero 2, ht_gt_zero] - have key_ne_zero : t ^ 2 + t + 1 ≠ 0 := ne_of_gt key_gt_zero have h₂ : x ≠ 1 := by rw [hx_t]; field_simp; linarith [key_gt_zero] have h₃ : y ≠ 1 := by rw [hy_t]; field_simp; linarith [key_gt_zero] have h₄ : z ≠ 1 := by rw [hz_t]; linarith [key_gt_zero] diff --git a/Archive/Imo/Imo2008Q4.lean b/Archive/Imo/Imo2008Q4.lean index a40e806a03290..97b1c519e5baa 100644 --- a/Archive/Imo/Imo2008Q4.lean +++ b/Archive/Imo/Imo2008Q4.lean @@ -48,10 +48,8 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) : rw [h w hw, h x hx, h (y ^ 2) (pow_pos hy 2), h (z ^ 2) (pow_pos hz 2)] · intro w x y z hw hx hy hz hprod rw [h w hw, h x hx, h (y ^ 2) (pow_pos hy 2), h (z ^ 2) (pow_pos hz 2)] - have hy2z2 : y ^ 2 + z ^ 2 ≠ 0 := ne_of_gt (add_pos (pow_pos hy 2) (pow_pos hz 2)) - have hz2y2 : z ^ 2 + y ^ 2 ≠ 0 := ne_of_gt (add_pos (pow_pos hz 2) (pow_pos hy 2)) have hp2 : w ^ 2 * x ^ 2 = y ^ 2 * z ^ 2 := by linear_combination (w * x + y * z) * hprod - field_simp [ne_of_gt hw, ne_of_gt hx, ne_of_gt hy, ne_of_gt hz, hy2z2, hz2y2, hp2] + field_simp [hp2] ring -- proof that the only solutions are f(x) = x or f(x) = 1/x intro H₂ @@ -66,7 +64,6 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) : have h1xss : 1 * x = sqrt x * sqrt x := by rw [one_mul, mul_self_sqrt (le_of_lt hx)] specialize H₂ 1 x (sqrt x) (sqrt x) zero_lt_one hx (sqrt_pos.mpr hx) (sqrt_pos.mpr hx) h1xss rw [h₁, one_pow 2, sq_sqrt (le_of_lt hx), ← two_mul (f x), ← two_mul x] at H₂ - have hx_ne_0 : x ≠ 0 := ne_of_gt hx have hfx_ne_0 : f x ≠ 0 := by specialize H₁ x hx; exact ne_of_gt H₁ field_simp at H₂ ⊢ linear_combination 1 / 2 * H₂ @@ -82,12 +79,12 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) : specialize H₂ a b (sqrt (a * b)) (sqrt (a * b)) ha hb (sqrt_pos.mpr hab) (sqrt_pos.mpr hab) habss rw [sq_sqrt (le_of_lt hab), ← two_mul (f (a * b)), ← two_mul (a * b)] at H₂ rw [hfa₂, hfb₂] at H₂ - have h2ab_ne_0 : 2 * (a * b) ≠ 0 := mul_ne_zero two_ne_zero (ne_of_gt hab) + have h2ab_ne_0 : 2 * (a * b) ≠ 0 := by positivity specialize h₃ (a * b) hab cases' h₃ with hab₁ hab₂ -- f(ab) = ab → b^4 = 1 → b = 1 → f(b) = b → false - · field_simp [hab₁] at H₂ - field_simp [ne_of_gt hb] at H₂ + · rw [ hab₁, div_left_inj' h2ab_ne_0 ] at H₂ + field_simp at H₂ have hb₁ : b ^ 4 = 1 := by linear_combination -H₂ obtain hb₂ := abs_eq_one_of_pow_eq_one b 4 (show 4 ≠ 0 by norm_num) hb₁ rw [abs_of_pos hb] at hb₂; rw [hb₂] at hfb₁; exact hfb₁ h₁ diff --git a/Archive/Imo/Imo2013Q1.lean b/Archive/Imo/Imo2013Q1.lean index dc5b2a7f66d14..1e1d62935567f 100644 --- a/Archive/Imo/Imo2013Q1.lean +++ b/Archive/Imo/Imo2013Q1.lean @@ -67,12 +67,11 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) : use m have hmpk : (m pk : ℚ) = 2 * t + 2 ^ pk.succ := by have : m pk = ⟨2 * t + 2 ^ pk.succ, _⟩ := if_neg (irrefl pk); simp [this] - have denom_ne_zero : (2 * (t : ℚ) + 2 * 2 ^ pk) ≠ 0 := by positivity calc ((1 : ℚ) + (2 ^ pk.succ - 1) / (n : ℚ) : ℚ)= 1 + (2 * 2 ^ pk - 1) / (2 * (t + 1) : ℕ) := by rw [ht, pow_succ] _ = (1 + 1 / (2 * t + 2 * 2 ^ pk)) * (1 + (2 ^ pk - 1) / (↑t + 1)) := by - field_simp [t.cast_add_one_ne_zero] + field_simp ring _ = (1 + 1 / (2 * t + 2 ^ pk.succ)) * (1 + (2 ^ pk - 1) / t_succ) := by -- porting note: used to work with `norm_cast` @@ -90,12 +89,11 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) : have hmpk : (m pk : ℚ) = 2 * t + 1 := by have : m pk = ⟨2 * t + 1, _⟩ := if_neg (irrefl pk) simp [this] - have denom_ne_zero : 2 * (t : ℚ) + 1 ≠ 0 := by norm_cast; apply (2 * t).succ_ne_zero calc ((1 : ℚ) + (2 ^ pk.succ - 1) / ↑n : ℚ) = 1 + (2 * 2 ^ pk - 1) / (2 * t + 1 : ℕ) := by rw [ht, pow_succ] _ = (1 + 1 / (2 * t + 1)) * (1 + (2 ^ pk - 1) / (t + 1)) := by - field_simp [t.cast_add_one_ne_zero] + field_simp ring _ = (1 + 1 / (2 * t + 1)) * (1 + (2 ^ pk - 1) / t_succ) := by norm_cast _ = (∏ i in Finset.range pk, (1 + 1 / (m i : ℚ))) * (1 + 1 / ↑(m pk)) := by diff --git a/Archive/Imo/Imo2013Q5.lean b/Archive/Imo/Imo2013Q5.lean index 98a3e482cc37d..668711c3df3cf 100644 --- a/Archive/Imo/Imo2013Q5.lean +++ b/Archive/Imo/Imo2013Q5.lean @@ -60,7 +60,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y) have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN have := calc - 1 = (x - y) * (1 / (x - y)) := by field_simp [ne_of_gt hxmy] + 1 = (x - y) * (1 / (x - y)) := by field_simp _ < (x - y) * N := by gcongr _ ≤ x ^ N - y ^ N := hn N hNp linarith [h N hNp] diff --git a/Archive/Wiedijk100Theorems/AreaOfACircle.lean b/Archive/Wiedijk100Theorems/AreaOfACircle.lean index e0277dfd4232f..d182d115fdb37 100644 --- a/Archive/Wiedijk100Theorems/AreaOfACircle.lean +++ b/Archive/Wiedijk100Theorems/AreaOfACircle.lean @@ -111,13 +111,13 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by ((hasDerivAt_const x (r : ℝ)⁻¹).mul (hasDerivAt_id' x)))).add ((hasDerivAt_id' x).mul ((((hasDerivAt_id' x).pow 2).const_sub ((r : ℝ) ^ 2)).sqrt _)) using 1 - · have h : sqrt ((1 : ℝ) - x ^ 2 / (r : ℝ) ^ 2) * r = sqrt ((r : ℝ) ^ 2 - x ^ 2) := by - rw [← sqrt_sq hle, ← sqrt_mul, sub_mul, sqrt_sq hle, mul_comm_div, - div_self (pow_ne_zero 2 hlt.ne'), one_mul, mul_one] - simpa [sqrt_sq hle, div_le_one (pow_pos hlt 2)] using sq_le_sq' hx1.le hx2.le + · have h₁ : (r:ℝ) ^ 2 - x ^ 2 > 0 := sub_pos_of_lt (sq_lt_sq' hx1 hx2) + have h : sqrt ((r:ℝ) ^ 2 - x ^ 2) ^ 3 = ((r:ℝ) ^ 2 - x ^ 2) * sqrt ((r: ℝ) ^ 2 - x ^ 2) := by + rw [pow_three, ← mul_assoc, mul_self_sqrt (by positivity)] field_simp - rw [h, mul_left_comm, ← sq, neg_mul_eq_mul_neg, mul_div_mul_left (-x ^ 2) _ two_ne_zero, - add_left_comm, div_add_div_same, ← sub_eq_add_neg, div_sqrt, two_mul] + ring_nf + rw [h] + ring · suffices -(1 : ℝ) < (r : ℝ)⁻¹ * x by exact this.ne' calc -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel hlt.ne'] diff --git a/Archive/Wiedijk100Theorems/InverseTriangleSum.lean b/Archive/Wiedijk100Theorems/InverseTriangleSum.lean index ca4556e94bc4d..24f64f26656d3 100644 --- a/Archive/Wiedijk100Theorems/InverseTriangleSum.lean +++ b/Archive/Wiedijk100Theorems/InverseTriangleSum.lean @@ -35,6 +35,6 @@ theorem Theorem100.inverse_triangle_sum : simp_rw [if_neg (Nat.succ_ne_zero _), Nat.succ_eq_add_one] have A : (n + 1 + 1 : ℚ) ≠ 0 := by norm_cast; norm_num push_cast - field_simp [Nat.cast_add_one_ne_zero] + field_simp ring #align theorem_100.inverse_triangle_sum Theorem100.inverse_triangle_sum diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean index 58ba2d6545bcc..25f5f89f832a9 100644 --- a/Mathlib/Algebra/Order/ToIntervalMod.lean +++ b/Mathlib/Algebra/Order/ToIntervalMod.lean @@ -1015,7 +1015,7 @@ theorem toIcoDiv_zero_one (b : α) : toIcoDiv (zero_lt_one' α) 0 b = ⌊b⌋ := theorem toIcoMod_eq_add_fract_mul (a b : α) : toIcoMod hp a b = a + Int.fract ((b - a) / p) * p := by rw [toIcoMod, toIcoDiv_eq_floor, Int.fract] - field_simp [hp.ne.symm] + field_simp ring #align to_Ico_mod_eq_add_fract_mul toIcoMod_eq_add_fract_mul @@ -1026,7 +1026,7 @@ theorem toIcoMod_eq_fract_mul (b : α) : toIcoMod hp 0 b = Int.fract (b / p) * p theorem toIocMod_eq_sub_fract_mul (a b : α) : toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p := by rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract] - field_simp [hp.ne.symm] + field_simp ring #align to_Ioc_mod_eq_sub_fract_mul toIocMod_eq_sub_fract_mul diff --git a/Mathlib/Algebra/QuadraticDiscriminant.lean b/Mathlib/Algebra/QuadraticDiscriminant.lean index c8315732262a0..5cb506af30a9a 100644 --- a/Mathlib/Algebra/QuadraticDiscriminant.lean +++ b/Mathlib/Algebra/QuadraticDiscriminant.lean @@ -134,7 +134,7 @@ theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a -- if a > 0 · have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1 - field_simp [ha.ne'] + field_simp ring #align discrim_le_zero discrim_le_zero diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index d4b0cd1b6ab40..08ece48f49cca 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -202,7 +202,7 @@ theorem isLittleO_of_lt_radius (h : ↑r < p.radius) : refine' ⟨_, rt, C, Or.inr zero_lt_one, fun n => _⟩ calc |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by - field_simp [mul_right_comm, abs_mul, this.ne'] + field_simp [mul_right_comm, abs_mul] _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC #align formal_multilinear_series.is_o_of_lt_radius FormalMultilinearSeries.isLittleO_of_lt_radius @@ -670,7 +670,7 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0} calc ‖(p n) fun _ : Fin n => y‖ _ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_op_norm _ _ - _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by field_simp [hr'0.ne', mul_right_comm] + _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by field_simp [mul_right_comm] _ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc] #align has_fpower_series_on_ball.uniform_geometric_approx' HasFPowerSeriesOnBall.uniform_geometric_approx' @@ -758,7 +758,7 @@ theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal _ = B n := by -- porting note: in the original, `B` was in the `field_simp`, but now Lean does not -- accept it. The current proof works in Lean 4, but does not in Lean 3. - field_simp [pow_succ, hr'0.ne'] + field_simp [pow_succ] simp only [mul_assoc, mul_comm, mul_left_comm] have hBL : HasSum B (L y) := by apply HasSum.mul_left diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index 42012071df3e2..036a07ecfaa51 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Basic.lean @@ -603,7 +603,7 @@ theorem dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq (h : Integra dist (∑ J in π₀.boxes, integralSum f vol (πi J)) (∑ J in π₀.boxes, integral J l f vol) := dist_triangle _ _ _ _ ≤ ε + δ' + ∑ _J in π₀.boxes, δ' := (add_le_add this (dist_sum_sum_le_of_le _ hπiδ')) - _ = ε + δ := by field_simp [H0.ne']; ring + _ = ε + δ := by field_simp; ring #align box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq /-- **Henstock-Sacks inequality**. Let `r : ℝⁿ → (0, ∞)` be a function such that for any tagged diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean index 938b8e6ea7857..dcf69d51c7ab5 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean @@ -139,7 +139,6 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) : exact ⟨R, fun x => hR (mem_range_self _)⟩ choose R hR using this let M := max (((Finset.range (n + 1)).image R).max' (by simp)) 1 - have M_pos : 0 < M := zero_lt_one.trans_le (le_max_right _ _) have δnpos : 0 < δ n := δpos n have IR : ∀ i ≤ n, R i ≤ M := by intro i hi @@ -157,7 +156,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) : _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by rw [norm_smul, Real.norm_of_nonneg]; positivity _ ≤ M⁻¹ * δ n * M := (mul_le_mul_of_nonneg_left ((hR i x).trans (IR i hi)) (by positivity)) - _ = δ n := by field_simp [M_pos.ne'] + _ = δ n := by field_simp choose r rpos hr using this have S : ∀ x, Summable fun n => (r n • g n) x := by intro x @@ -328,7 +327,7 @@ variable (E) theorem w_integral {D : ℝ} (Dpos : 0 < D) : ∫ x : E, w D x ∂μ = 1 := by simp_rw [w, integral_smul] rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm] - field_simp [Dpos.ne', (u_int_pos E).ne'] + field_simp [(u_int_pos E).ne'] #align exists_cont_diff_bump_base.W_integral ExistsContDiffBumpBase.w_integral theorem w_support {D : ℝ} (Dpos : 0 < D) : support (w D : E → ℝ) = ball 0 D := by @@ -557,7 +556,7 @@ instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E calc 2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) * 1 := mul_le_mul_of_nonneg_left hx (div_nonneg zero_le_two A.le) - _ = 1 - (R - 1) / (R + 1) := by field_simp [A.ne']; ring + _ = 1 - (R - 1) / (R + 1) := by field_simp; ring support := fun R hR => by have A : 0 < (R + 1) / 2 := by linarith have A' : 0 < R + 1 := by linarith @@ -565,8 +564,7 @@ instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E simp only [hR, if_true, support_comp_inv_smul₀ A.ne', y_support _ (IR R hR) C, _root_.smul_ball A.ne', Real.norm_of_nonneg A.le, smul_zero] refine' congr (congr_arg ball (Eq.refl 0)) _ - field_simp [A'.ne'] - ring } + field_simp; ring } end ExistsContDiffBumpBase diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean index 15b0c76bd8355..863930baaaddf 100644 --- a/Mathlib/Analysis/Calculus/Taylor.lean +++ b/Mathlib/Analysis/Calculus/Taylor.lean @@ -162,15 +162,11 @@ theorem hasDerivWithinAt_taylor_coeff_within {f : ℝ → E} {x y : ℝ} {k : (-((k ! : ℝ)⁻¹ * (x - y) ^ k)) t y := by -- Commuting the factors: have : -((k ! : ℝ)⁻¹ * (x - y) ^ k) = ((k + 1 : ℝ) * k !)⁻¹ * (-(k + 1) * (x - y) ^ k) := by - field_simp [k.factorial_ne_zero] - -- Porting note: was `ring_nf` - rw [mul_div_mul_right, ← neg_add_rev, neg_mul, neg_div, mul_div_cancel_left] - · exact k.cast_add_one_ne_zero - · simp [k.factorial_ne_zero] + field_simp; ring rw [this] exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _ convert this.smul hf using 1 - field_simp [Nat.cast_add_one_ne_zero k, Nat.factorial_ne_zero k] + field_simp rw [neg_div, neg_smul, sub_eq_add_neg] #align has_deriv_within_at_taylor_coeff_within hasDerivWithinAt_taylor_coeff_within @@ -256,7 +252,7 @@ theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : simp only [taylorWithinEval_self] at h rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel _ (g'_ne y hy)] at h rw [← h] - field_simp [g'_ne y hy, n.factorial_ne_zero] + field_simp [g'_ne y hy] ring #align taylor_mean_remainder taylor_mean_remainder @@ -289,16 +285,7 @@ theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ use y, hy simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h rw [h, neg_div, ← div_neg, neg_mul, neg_neg] - field_simp - -- Porting note: was `ring` - conv_lhs => - arg 2 - rw [← mul_assoc, mul_comm] - rw [mul_assoc, mul_div_mul_left _ _ (xy_ne y hy)] - conv_lhs => - arg 2 - rw [mul_comm] - nth_rw 1 [mul_comm] + field_simp [xy_ne y hy]; ring #align taylor_mean_remainder_lagrange taylor_mean_remainder_lagrange /-- **Taylor's theorem** with the Cauchy form of the remainder. diff --git a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean index f74454fe85b98..55bb0e2b6e0c4 100644 --- a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean +++ b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean @@ -61,7 +61,7 @@ theorem norm_cderiv_le (hr : 0 < r) (hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M) have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1 simp only [cderiv, norm_smul] refine' (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq _) - field_simp [_root_.abs_of_nonneg Real.pi_pos.le, Real.pi_pos.ne.symm, hr.ne.symm] + field_simp [_root_.abs_of_nonneg Real.pi_pos.le] ring #align complex.norm_cderiv_le Complex.norm_cderiv_le diff --git a/Mathlib/Analysis/Convex/Slope.lean b/Mathlib/Analysis/Convex/Slope.lean index cdc1c699060fe..a5b839f7560e9 100644 --- a/Mathlib/Analysis/Convex/Slope.lean +++ b/Mathlib/Analysis/Convex/Slope.lean @@ -32,18 +32,14 @@ theorem ConvexOn.slope_mono_adjacent (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx linarith set a := (z - y) / (z - x) set b := (y - x) / (z - x) - have hy : a • x + b • z = y := by - field_simp - rw [div_eq_iff] <;> [ring; linarith] + have hy : a • x + b • z = y := by field_simp; ring have key := hf.2 hx hz (show 0 ≤ a by apply div_nonneg <;> linarith) (show 0 ≤ b by apply div_nonneg <;> linarith) - (show a + b = 1 by - field_simp - rw [div_eq_iff] <;> [ring; linarith]) + (show a + b = 1 by field_simp) rw [hy] at key replace key := mul_le_mul_of_nonneg_left key hxz.le - field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢ + field_simp [mul_comm (z - x) _] at key ⊢ rw [div_le_div_right] · linarith · nlinarith @@ -72,17 +68,13 @@ theorem StrictConvexOn.slope_strict_mono_adjacent (hf : StrictConvexOn 𝕜 s f) linarith set a := (z - y) / (z - x) set b := (y - x) / (z - x) - have hy : a • x + b • z = y := by - field_simp - rw [div_eq_iff] <;> [ring; linarith] + have hy : a • x + b • z = y := by field_simp; ring have key := hf.2 hx hz hxz' (div_pos hyz hxz) (div_pos hxy hxz) - (show a + b = 1 by - field_simp - rw [div_eq_iff] <;> [ring; linarith]) + (show a + b = 1 by field_simp) rw [hy] at key replace key := mul_lt_mul_of_pos_left key hxz - field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢ + field_simp [mul_comm (z - x) _] at key ⊢ rw [div_lt_div_right] · linarith · nlinarith @@ -247,12 +239,12 @@ theorem ConvexOn.secant_mono_aux1 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : _ ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := hf.2 hx hz ha hb ?_ _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_ · congr 1 - field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] + field_simp ring · -- Porting note: this `show` wasn't needed in Lean 3 show (z - y) / (z - x) + (y - x) / (z - x) = 1 - field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] - · field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] + field_simp + · field_simp #align convex_on.secant_mono_aux1 ConvexOn.secant_mono_aux1 theorem ConvexOn.secant_mono_aux2 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) @@ -297,12 +289,12 @@ theorem StrictConvexOn.secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 s f) {x _ < (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := (hf.2 hx hz (by linarith) ha hb ?_) _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_ · congr 1 - field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] + field_simp ring · -- Porting note: this `show` wasn't needed in Lean 3 show (z - y) / (z - x) + (y - x) / (z - x) = 1 - field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] - · field_simp [hxy'.ne', hyz'.ne', hxz'.ne'] + field_simp + · field_simp #align strict_convex_on.secant_strict_mono_aux1 StrictConvexOn.secant_strict_mono_aux1 theorem StrictConvexOn.secant_strict_mono_aux2 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean index 9d629aa510d9c..3ca7e9e3e1587 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean @@ -130,7 +130,7 @@ theorem convexOn_zpow : ∀ m : ℤ, ConvexOn ℝ (Ioi 0) fun x : ℝ => x ^ m simp_rw [zpow_negSucc] refine' ⟨convex_Ioi _, _⟩ rintro a (ha : 0 < a) b (hb : 0 < b) μ ν hμ hν h - field_simp [ha.ne', hb.ne'] + field_simp rw [div_le_div_iff] · -- Porting note: added type ascription to LHS calc @@ -168,7 +168,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by calc log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne'] _ < z / y - 1 := (log_lt_sub_one_of_pos hyz' hyz'') - _ = y⁻¹ * (z - y) := by field_simp [hy.ne'] + _ = y⁻¹ * (z - y) := by field_simp · have h : 0 < y - x := by linarith rw [lt_div_iff h] have hxy' : 0 < x / y := by positivity @@ -177,7 +177,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by rw [div_eq_one_iff_eq hy.ne'] at h simp [h] calc - y⁻¹ * (y - x) = 1 - x / y := by field_simp [hy.ne'] + y⁻¹ * (y - x) = 1 - x / y := by field_simp _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy''] _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne'] _ = log y - log x := by ring @@ -204,16 +204,16 @@ theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ -- but now Lean doesn't guess we are talking about `1` fast enough. haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1 - · field_simp [log_one] - · field_simp [log_one] + · field_simp + · field_simp · nlinarith · rw [← div_lt_iff hp, ← div_lt_div_right hs'] -- Porting note: previously we could write `zero_lt_one` inline, -- but now Lean doesn't guess we are talking about `1` fast enough. haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1 - · field_simp [log_one, hp.ne'] - · field_simp [log_one] + · field_simp + · field_simp · nlinarith #align one_add_mul_self_lt_rpow_one_add one_add_mul_self_lt_rpow_one_add @@ -251,10 +251,10 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) convert this using 1 · have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _ ring_nf at H ⊢ - field_simp [hy.ne', hy'.ne'] at H ⊢ + field_simp at H ⊢ linear_combination H · ring_nf at H1 ⊢ - field_simp [hy.ne', hy'.ne'] + field_simp linear_combination p * (-y + x) * H1 · have hyz' : 0 < z - y := by linarith only [hyz] have hyz'' : 1 < z / y := by rwa [one_lt_div hy] @@ -265,11 +265,11 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) rw [lt_div_iff hyz', ← div_lt_div_right hy'] convert this using 1 · ring_nf at H1 ⊢ - field_simp [hy.ne', hy'.ne'] at H1 ⊢ + field_simp at H1 ⊢ linear_combination p * (y - z) * y ^ p * H1 · have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _ ring_nf at H ⊢ - field_simp [hy.ne', hy'.ne'] at H ⊢ + field_simp at H ⊢ linear_combination -H #align strict_convex_on_rpow strictConvexOn_rpow diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean index 37a815589225b..cd4ce864acbd0 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean @@ -147,7 +147,9 @@ theorem deriv2_sqrt_mul_log (x : ℝ) : convert (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <| mul_ne_zero two_ne_zero h₀).deriv using 1 nth_rw 3 [← mul_self_sqrt hx.le] - field_simp; ring + generalize sqrt x = sqx at h₀ -- else field_simp rewrites sqrt x * sqrt x back to x + field_simp + ring #align deriv2_sqrt_mul_log deriv2_sqrt_mul_log theorem strictConcaveOn_sqrt_mul_log_Ioi : diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index d2a28b998feab..b4ec1644944da 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -109,7 +109,7 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul] use m - field_simp [Real.two_pi_pos.ne'] at hm + field_simp at hm rw [← mul_right_inj' Real.two_pi_pos.ne'] linarith #align add_circle.injective_to_circle AddCircle.injective_toCircle diff --git a/Mathlib/Analysis/NormedSpace/Pointwise.lean b/Mathlib/Analysis/NormedSpace/Pointwise.lean index db9e90959d97f..af8038672bf34 100644 --- a/Mathlib/Analysis/NormedSpace/Pointwise.lean +++ b/Mathlib/Analysis/NormedSpace/Pointwise.lean @@ -131,7 +131,7 @@ theorem eventually_singleton_add_smul_subset {x : E} {s : Set E} (hs : Bounded s _ ≤ ε / R * R := (mul_le_mul (mem_closedBall_zero_iff.1 hr) (mem_closedBall_zero_iff.1 (hR zs)) (norm_nonneg _) (div_pos εpos Rpos).le) - _ = ε := by field_simp [Rpos.ne'] + _ = ε := by field_simp have : y = x + r • z := by simp only [hz, add_neg_cancel_left] apply hε simpa only [this, dist_eq_norm, add_sub_cancel', mem_closedBall] using I diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean index 615eea7cdf3ac..b656b252641bd 100644 --- a/Mathlib/Analysis/NormedSpace/lpSpace.lean +++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean @@ -417,7 +417,7 @@ theorem norm_eq_tsum_rpow (hp : 0 < p.toReal) (f : lp E p) : theorem norm_rpow_eq_tsum (hp : 0 < p.toReal) (f : lp E p) : ‖f‖ ^ p.toReal = ∑' i, ‖f i‖ ^ p.toReal := by rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul] - · field_simp [hp.ne'] + · field_simp apply tsum_nonneg intro i calc diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean index 8ffad18b00163..2b47876fb71f3 100644 --- a/Mathlib/Analysis/PSeries.lean +++ b/Mathlib/Analysis/PSeries.lean @@ -304,7 +304,7 @@ theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) : 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 [B.ne'] + field_simp rw [div_le_div_iff _ A, ← sub_nonneg] · ring_nf rw [add_comm] diff --git a/Mathlib/Analysis/SpecialFunctions/Stirling.lean b/Mathlib/Analysis/SpecialFunctions/Stirling.lean index 58b0c1be06d24..a18ca039b7438 100644 --- a/Mathlib/Analysis/SpecialFunctions/Stirling.lean +++ b/Mathlib/Analysis/SpecialFunctions/Stirling.lean @@ -90,8 +90,6 @@ theorem log_stirlingSeq_diff_hasSum (m : ℕ) : · ext k rw [← pow_mul, pow_add] push_cast - have : 2 * (k : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * k) - have : 2 * ((m : ℝ) + 1) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * m.succ) field_simp ring · have h : ∀ (x : ℝ) (_ : x ≠ 0), 1 + x⁻¹ = (x + 1) / x := by @@ -235,13 +233,7 @@ theorem stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq (n : ℕ) (hn : n ≠ 0) simp_rw [div_pow, mul_pow] rw [sq_sqrt, sq_sqrt] any_goals positivity - have : (n : ℝ) ≠ 0 := cast_ne_zero.mpr hn - have : exp 1 ≠ 0 := exp_ne_zero 1 - have : ((2 * n)! : ℝ) ≠ 0 := cast_ne_zero.mpr (factorial_ne_zero (2 * n)) - have : 2 * (n : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * n) - field_simp - simp only [mul_pow, mul_comm 2 n, mul_comm 4 n, pow_mul] - ring + field_simp; ring #align stirling.stirling_seq_pow_four_div_stirling_seq_pow_two_eq Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq /-- Suppose the sequence `stirlingSeq` (defined above) has the limit `a ≠ 0`. diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean index 75afcef45e99f..ec1f1b2706d82 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson -/ import Mathlib.Analysis.SpecialFunctions.Exp +import Mathlib.Tactic.Positivity.Core #align_import analysis.special_functions.trigonometric.basic from "leanprover-community/mathlib"@"2c1d8ca2812b64f88992a5294ea3dba144755cd1" @@ -163,6 +164,17 @@ theorem pi_pos : 0 < π := lt_of_lt_of_le (by norm_num) two_le_pi #align real.pi_pos Real.pi_pos +namespace Mathlib.Meta.Positivity +open Lean.Meta Qq + +/-- Extension for the `positivity` tactic: `π` is always positive. -/ +@[positivity π] +def evalExp : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ _ := do + pure (.positive (q(Real.pi_pos) : Lean.Expr)) + +end Mathlib.Meta.Positivity + + theorem pi_ne_zero : π ≠ 0 := ne_of_gt pi_pos #align real.pi_ne_zero Real.pi_ne_zero diff --git a/Mathlib/Combinatorics/Catalan.lean b/Mathlib/Combinatorics/Catalan.lean index e628af38c62e3..58f251ddf6073 100644 --- a/Mathlib/Combinatorics/Catalan.lean +++ b/Mathlib/Combinatorics/Catalan.lean @@ -87,12 +87,10 @@ private def gosperCatalan (n j : ℕ) : ℚ := private theorem gosper_trick {n i : ℕ} (h : i ≤ n) : gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = Nat.centralBinom i / (i + 1) * Nat.centralBinom (n - i) / (n - i + 1) := by - have l₁ : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact n.succ_ne_zero - have l₂ : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero - have l₃ : (i : ℚ) + 1 ≠ 0 := by norm_cast; exact i.succ_ne_zero - have l₄ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast; exact (n - i).succ_ne_zero - have h₁ := (mul_div_cancel_left (↑(Nat.centralBinom (i + 1))) l₃).symm - have h₂ := (mul_div_cancel_left (↑(Nat.centralBinom (n - i + 1))) l₄).symm + have l₁ : (i : ℚ) + 1 ≠ 0 := by norm_cast; exact i.succ_ne_zero + have l₂ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast; exact (n - i).succ_ne_zero + have h₁ := (mul_div_cancel_left (↑(Nat.centralBinom (i + 1))) l₁).symm + have h₂ := (mul_div_cancel_left (↑(Nat.centralBinom (n - i + 1))) l₂).symm have h₃ : ((i : ℚ) + 1) * (i + 1).centralBinom = 2 * (2 * i + 1) * i.centralBinom := by exact_mod_cast Nat.succ_mul_centralBinom_succ i have h₄ : diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index b2f25d884b168..f1d7b052b0e84 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/Mathlib/Data/Complex/Exponential.lean @@ -907,7 +907,6 @@ theorem cos_sub_cos : cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2) #align complex.cos_sub_cos Complex.cos_sub_cos theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := by - have h2 : (2 : ℂ) ≠ 0 := by norm_num calc cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_ _ = @@ -916,7 +915,7 @@ theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) ?_ _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_ - · congr <;> field_simp [h2] + · congr <;> field_simp · rw [cos_add, cos_sub] ring #align complex.cos_add_cos Complex.cos_add_cos @@ -1046,9 +1045,8 @@ theorem sin_sq : sin x ^ 2 = 1 - cos x ^ 2 := by rw [← sin_sq_add_cos_sq x, ad #align complex.sin_sq Complex.sin_sq theorem inv_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2 := by - have : cos x ^ 2 ≠ 0 := pow_ne_zero 2 hx rw [tan_eq_sin_div_cos, div_pow] - field_simp [this] + field_simp #align complex.inv_one_add_tan_sq Complex.inv_one_add_tan_sq theorem tan_sq_div_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) : @@ -2001,7 +1999,7 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t · abel · rw [← Real.exp_nat_mul] congr 1 - field_simp [(Nat.cast_ne_zero (R := ℝ)).mpr hn] + field_simp ring_nf · rwa [add_comm, ← sub_eq_add_neg, sub_nonneg, div_le_one] positivity diff --git a/Mathlib/Data/Polynomial/HasseDeriv.lean b/Mathlib/Data/Polynomial/HasseDeriv.lean index 59a575522d531..4803857c9d496 100644 --- a/Mathlib/Data/Polynomial/HasseDeriv.lean +++ b/Mathlib/Data/Polynomial/HasseDeriv.lean @@ -188,9 +188,7 @@ theorem hasseDeriv_comp (k l : ℕ) : rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl] rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub] simp only [add_tsub_cancel_left] - have H : ∀ n : ℕ, (n ! : ℚ) ≠ 0 := by exact_mod_cast factorial_ne_zero - field_simp [H] - ring + field_simp; ring #align polynomial.hasse_deriv_comp Polynomial.hasseDeriv_comp theorem natDegree_hasseDeriv_le (p : R[X]) (n : ℕ) : diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index 225c8fdfe0235..8c1e43eaf5551 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -236,12 +236,6 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) have ha : 1 - a ≠ 0 := by have : a < 1 := (inner_lt_one_iff_real_of_norm_one hv (by simp)).mpr hx.symm linarith - have : 2 ^ 2 * ‖y‖ ^ 2 + 4 * (1 - a) ^ 2 ≠ 0 := by - refine' ne_of_gt _ - have : (0 : ℝ) < (1 - a) ^ 2 := sq_pos_of_ne_zero (1 - a) ha - -- Porting note: nlinarith needed a little help - change 0 < 4 * _ + 4 * _ - nlinarith -- the core of the problem is these two algebraic identities: have h₁ : (2 ^ 2 / (1 - a) ^ 2 * ‖y‖ ^ 2 + 4)⁻¹ * 4 * (2 / (1 - a)) = 1 := by -- Porting note: used to be `field_simp; simp only [Submodule.coe_norm] at *; nlinarith` @@ -250,21 +244,15 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) -- clear_value because field_simp does zeta-reduction (by design?) and is annoying clear_value a y field_simp - rw [div_eq_iff, duh] - · ring - · apply mul_ne_zero_iff.mpr ⟨?_,ha⟩ - convert this using 2; rw [Submodule.coe_norm]; ring + rw [duh] + ring have h₂ : (2 ^ 2 / (1 - a) ^ 2 * ‖y‖ ^ 2 + 4)⁻¹ * (2 ^ 2 / (1 - a) ^ 2 * ‖y‖ ^ 2 - 4) = a := by -- Porting note: field_simp is not behaving as in ml3 -- see porting note above; previous proof used trans and was comparably complicated clear_value a y field_simp - rw [div_eq_iff, duh] - ring_nf - -- Porting note: shouldn't repeat myself but getting the coercion right is annoying - apply mul_ne_zero_iff.mpr ⟨?_,?_⟩ - · convert this using 2; rw [Submodule.coe_norm]; ring - · apply pow_ne_zero _ ha + rw [duh] + ring convert congr_arg₂ Add.add (congr_arg (fun t => t • (y : E)) h₁) (congr_arg (fun t => t • v) h₂) using 1 · simp [inner_add_right, inner_smul_right, hvy, real_inner_self_eq_norm_mul_norm, hv, mul_smul, @@ -281,10 +269,7 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) theorem stereo_right_inv (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : stereoToFun v (stereoInvFun hv w) = w := by have : 2 / (1 - (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4)) * (‖(w : E)‖ ^ 2 + 4)⁻¹ * 4 = 1 := by - have : ‖(w : E)‖ ^ 2 + 4 ≠ 0 := by nlinarith - have : (4 : ℝ) + 4 ≠ 0 := by nlinarith - field_simp - ring + field_simp; ring convert congr_arg (· • w) this · have h₁ : orthogonalProjection (ℝ ∙ v)ᗮ v = 0 := orthogonalProjection_orthogonalComplement_singleton_eq_zero v diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 2d3ff7c91a9e5..efdfc4623f5c3 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -175,7 +175,7 @@ theorem bernoulli'PowerSeries_mul_exp_sub_one : have := factorial_mul_factorial_dvd_factorial_add i j field_simp [mul_comm _ (bernoulli' i), mul_assoc, add_choose] norm_cast - rw [mul_comm (j + 1), mul_div_assoc, ← mul_assoc] + simp [mul_comm (j + 1)] #align bernoulli'_power_series_mul_exp_sub_one bernoulli'PowerSeries_mul_exp_sub_one /-- Odd Bernoulli numbers (greater than 1) are zero. -/ @@ -292,12 +292,11 @@ theorem bernoulliPowerSeries_mul_exp_sub_one : bernoulliPowerSeries A * (exp A - rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div] refine' congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) _) rw [mem_antidiagonal] at h - have hj : (x.2 + 1 : ℚ) ≠ 0 := by norm_cast; exact succ_ne_zero _ rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)] - field_simp [mul_ne_zero hj (hfact x.2), hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc, - Nat.factorial_ne_zero, hj] + field_simp [hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc] -- porting note: was `cc`, which was not yet ported left + left ring #align bernoulli_power_series_mul_exp_sub_one bernoulliPowerSeries_mul_exp_sub_one @@ -371,7 +370,7 @@ theorem sum_range_pow (n p : ℕ) : -- massage `hps` into our goal rw [hps, sum_mul] refine' sum_congr rfl fun x _ => _ - field_simp [mul_right_comm _ ↑p !, ← mul_assoc _ _ ↑p !, cast_add_one_ne_zero, hne] + field_simp [mul_right_comm _ ↑p !, ← mul_assoc _ _ ↑p !] ring #align sum_range_pow sum_range_pow diff --git a/Mathlib/NumberTheory/DiophantineApproximation.lean b/Mathlib/NumberTheory/DiophantineApproximation.lean index fbeb693d1aaef..10eb81d0ac11e 100644 --- a/Mathlib/NumberTheory/DiophantineApproximation.lean +++ b/Mathlib/NumberTheory/DiophantineApproximation.lean @@ -427,7 +427,7 @@ private theorem aux₁ : 0 < fract ξ := by have H : (2 * v - 1 : ℝ) < 1 := by refine' (mul_lt_iff_lt_one_right hv₀).mp ((inv_lt_inv hv₀ (mul_pos hv₁ hv₂)).mp (lt_of_le_of_lt _ h)) - have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field_simp [hv₀.ne'] + have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field_simp rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_right hv₀] norm_cast rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero] @@ -491,7 +491,7 @@ private theorem aux₃ : have H : (2 * u' - 1 : ℝ) ≤ (2 * v - 1) * fract ξ := by replace h := (abs_lt.mp h).1 have : (2 * (v : ℝ) - 1) * (-((v : ℝ) * (2 * v - 1))⁻¹ + u' / v) = 2 * u' - (1 + u') / v := by - field_simp [Hv.ne', Hv'.ne']; ring + field_simp; ring rw [hu'ℝ, add_div, mul_div_cancel _ Hv.ne', ← sub_sub, sub_right_comm, self_sub_floor, lt_sub_iff_add_lt, ← mul_lt_mul_left Hv', this] at h refine' LE.le.trans _ h.le @@ -517,12 +517,11 @@ private theorem invariant : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ refine' ⟨_, fun huv => _, by exact_mod_cast aux₃ hv h⟩ · rw [sub_eq_add_neg, ← neg_mul, isCoprime_comm, IsCoprime.add_mul_right_left_iff] exact h.1 - · obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv) + · obtain hv₀' := (aux₀ (zero_lt_two.trans_le hv)).2 have Hv : (v * (2 * v - 1) : ℝ)⁻¹ + (v : ℝ)⁻¹ = 2 / (2 * v - 1) := by - field_simp [hv₀.ne', hv₀'.ne'] - ring + field_simp; ring have Huv : (u / v : ℝ) = ⌊ξ⌋ + (v : ℝ)⁻¹ := by - rw [sub_eq_iff_eq_add'.mp huv]; field_simp [hv₀.ne'] + rw [sub_eq_iff_eq_add'.mp huv]; field_simp have h' := (abs_sub_lt_iff.mp h.2.2).1 rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h' rwa [lt_sub_iff_add_lt', (by ring : (v : ℝ) + -(1 / 2) = (2 * v - 1) / 2), diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean index 4b78ec480ae81..2392e781b2dd6 100644 --- a/Mathlib/NumberTheory/PythagoreanTriples.lean +++ b/Mathlib/NumberTheory/PythagoreanTriples.lean @@ -460,13 +460,11 @@ theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (h · exact h.isPrimitiveClassified_of_coprime_of_zero_left hc h0 let v := (x : ℚ) / z let w := (y : ℚ) / z - have hz : z ≠ 0 - apply ne_of_gt hzpos have hq : v ^ 2 + w ^ 2 = 1 := by - field_simp [hz, sq] + field_simp [sq] norm_cast have hvz : v ≠ 0 := by - field_simp [hz] + field_simp exact h0 have hw1 : w ≠ -1 := by contrapose! hvz with hw1 diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean index ae9051bc09a02..2fec077bd662b 100644 --- a/Mathlib/Tactic/FieldSimp.lean +++ b/Mathlib/Tactic/FieldSimp.lean @@ -8,6 +8,7 @@ import Lean.Elab.Tactic.Basic import Lean.Meta.Tactic.Simp.Main import Std.Lean.Parser import Mathlib.Algebra.Group.Units +import Mathlib.Tactic.Positivity.Core import Mathlib.Tactic.NormNum.Core import Qq @@ -34,9 +35,11 @@ private def dischargerTraceMessage (prop: Expr) : Except ε (Option Expr) → Si /-- Discharge strategy for the `field_simp` tactic. -/ partial def discharge (prop : Expr) : SimpM (Option Expr) := withTraceNode `Tactic.field_simp (dischargerTraceMessage prop) do + -- Discharge strategy 1: Use assumptions if let some r ← Simp.dischargeUsingAssumption? prop then return some r + -- Discharge strategy 2: Normalize inequalities using NormNum let prop : Q(Prop) ← (do pure prop) let pf? ← match prop with | ~q(($e : $α) ≠ $b) => @@ -50,6 +53,13 @@ partial def discharge (prop : Expr) : SimpM (Option Expr) := | _ => pure none if let some pf := pf? then return some pf + -- Discharge strategy 3: Use positivity + let pf? ← + try some <$> Mathlib.Meta.Positivity.solve prop + catch _ => pure none + if let some pf := pf? then return some pf + + -- Discharge strategy 4: Use the simplifier let ctx ← read let usedTheorems := (← get).usedTheorems diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 58ab9611a75f6..e9a98c80b2c56 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -311,12 +311,11 @@ private inductive OrderRel : Type end Meta.Positivity namespace Meta.Positivity -/-- The main entry point to the `positivity` tactic. Given a goal `goal` of the form `0 [≤/ throw "nonzeroness" "nonnegativity" | _, .none => throwError "failed to prove positivity/nonnegativity/nonzeroness" - goal.assign p + pure p match t with | ~q(@LE.le $α $_a $z $e) => rest α z e .le | ~q(@LT.lt $α $_a $z $e) => rest α z e .lt @@ -352,6 +351,14 @@ def positivity (goal : MVarId) : MetaM Unit := do rest α a b .ne' | _ => throwError "not a positivity goal" +/-- The main entry point to the `positivity` tactic. Given a goal `goal` of the form `0 [≤/