diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean index c5e69f5e9a19f..f21958832dbda 100644 --- a/Mathlib/Algebra/Polynomial/Module/Basic.lean +++ b/Mathlib/Algebra/Polynomial/Module/Basic.lean @@ -276,8 +276,7 @@ theorem eval_smul (p : R[X]) (q : PolynomialModule R M) (r : R) : intro i m induction p using Polynomial.induction_on' with | h_add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul] - | h_monomial => rw [monomial_smul_single, eval_single, Polynomial.eval_monomial, eval_single, - smul_comm, ← smul_smul, pow_add, mul_smul] + | h_monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module @[simp] theorem eval_map (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) : @@ -287,7 +286,8 @@ theorem eval_map (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) : · intro f g e₁ e₂ simp_rw [map_add, e₁, e₂] · intro i m - rw [map_single, eval_single, eval_single, f.map_smul, ← map_pow, algebraMap_smul] + simp only [map_single, eval_single, f.map_smul] + module @[simp] theorem eval_map' (f : M →ₗ[R] M) (q : PolynomialModule R M) (r : R) : @@ -324,8 +324,8 @@ theorem comp_eval (p : R[X]) (q : PolynomialModule R M) (r : R) : · intro _ _ e₁ e₂ simp_rw [map_add, e₁, e₂] · intro i m - rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, pow_zero, one_smul, - Polynomial.eval_pow] + rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow] + module theorem comp_smul (p p' : R[X]) (q : PolynomialModule R M) : comp p (p' • q) = p'.comp p • comp p q := by diff --git a/Mathlib/Analysis/Analytic/Meromorphic.lean b/Mathlib/Analysis/Analytic/Meromorphic.lean index 4c3349d87d078..be73e28bbbfe1 100644 --- a/Mathlib/Analysis/Analytic/Meromorphic.lean +++ b/Mathlib/Analysis/Analytic/Meromorphic.lean @@ -59,8 +59,8 @@ lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f rcases hg with ⟨n, hg⟩ refine ⟨m + n, ?_⟩ convert hf.smul hg using 2 with z - rw [smul_eq_mul, ← mul_smul, mul_assoc, mul_comm (f z), ← mul_assoc, pow_add, - ← smul_eq_mul (a' := f z), smul_assoc, Pi.smul_apply'] + rw [Pi.smul_apply', smul_eq_mul] + module lemma mul {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (f * g) x := @@ -227,8 +227,8 @@ lemma iff_eventuallyEq_zpow_smul_analyticAt {f : 𝕜 → E} {x : 𝕜} : Meromo ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩ · filter_upwards with z hz - rw [← mul_smul, ← zpow_natCast, ← zpow_add₀ (sub_ne_zero.mpr hz), neg_add_cancel, - zpow_zero, one_smul] + match_scalars + field_simp [sub_ne_zero.mpr hz] · refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq) exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt diff --git a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean index 1835d8c1d6fa5..399dada358cca 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean @@ -97,8 +97,8 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) rw [← smul_smul] apply s_conv.interior.add_smul_mem this _ ht rw [add_assoc] at hw - rw [add_assoc, ← smul_add] - exact s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ + convert s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ using 1 + module -- define a function `g` on `[0,1]` (identified with `[v, v + w]`) such that `g 1 - g 0` is the -- quantity to be estimated. We will check that its derivative is given by an explicit -- expression `g'`, that we can bound. Then the desired bound for `g 1 - g 0` follows from the @@ -139,14 +139,14 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) calc ‖g' t‖ = ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖ := by rw [hg'] - have : h * (t * h) = t * (h * h) := by ring - simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.map_add, pow_two, - ContinuousLinearMap.add_apply, Pi.smul_apply, smul_sub, smul_add, smul_smul, ← sub_sub, - ContinuousLinearMap.coe_smul', Pi.sub_apply, ContinuousLinearMap.map_smul, this] + congrm ‖?_‖ + simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply, + ContinuousLinearMap.smul_apply, map_add, map_smul] + module _ ≤ ‖f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)‖ * ‖h • w‖ := (ContinuousLinearMap.le_opNorm _ _) _ ≤ ε * ‖h • v + (t * h) • w‖ * ‖h • w‖ := by - apply mul_le_mul_of_nonneg_right _ (norm_nonneg _) + gcongr have H : x + h • v + (t * h) • w ∈ Metric.ball x δ ∩ interior s := by refine ⟨?_, xt_mem t ⟨ht.1, ht.2.le⟩⟩ rw [add_assoc, add_mem_ball_iff_norm] @@ -157,7 +157,7 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) apply (norm_add_le _ _).trans gcongr simp only [norm_smul, Real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc] - exact mul_le_of_le_one_left (mul_nonneg hpos.le (norm_nonneg _)) ht.2.le + exact mul_le_of_le_one_left (by positivity) ht.2.le _ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by simp only [norm_smul, Real.norm_eq_abs, abs_mul, abs_of_nonneg, hpos.le]; ring -- conclude using the mean value inequality @@ -169,8 +169,8 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) simp only [g, Nat.one_ne_zero, add_zero, one_mul, zero_div, zero_mul, sub_zero, zero_smul, Ne, not_false_iff, zero_pow, reduceCtorEq] abel - · simp only [Real.norm_eq_abs, abs_mul, add_nonneg (norm_nonneg v) (norm_nonneg w), abs_of_nonneg, - hpos.le, mul_assoc, norm_nonneg, abs_pow] + · simp (discharger := positivity) only [Real.norm_eq_abs, abs_mul, abs_of_nonneg, abs_pow] + ring /-- One can get `f'' v w` as the limit of `h ^ (-2)` times the alternate sum of the values of `f` along the vertices of a quadrilateral with sides `h v` and `h w` based at `x`. @@ -183,40 +183,27 @@ theorem Convex.isLittleO_alternate_sum_square {v w : E} (h4v : x + (4 : ℝ) • fun h => h ^ 2 := by have A : (1 : ℝ) / 2 ∈ Ioc (0 : ℝ) 1 := ⟨by norm_num, by norm_num⟩ have B : (1 : ℝ) / 2 ∈ Icc (0 : ℝ) 1 := ⟨by norm_num, by norm_num⟩ - have C : ∀ w : E, (2 : ℝ) • w = 2 • w := fun w => by simp only [two_smul] have h2v2w : x + (2 : ℝ) • v + (2 : ℝ) • w ∈ interior s := by convert s_conv.interior.add_smul_sub_mem h4v h4w B using 1 - simp only [smul_sub, smul_smul, one_div, add_sub_add_left_eq_sub, mul_add, add_smul] - norm_num - simp only [show (4 : ℝ) = (2 : ℝ) + (2 : ℝ) by norm_num, _root_.add_smul] - abel + module have h2vww : x + (2 • v + w) + w ∈ interior s := by convert h2v2w using 1 - simp only [two_smul] - abel + module have h2v : x + (2 : ℝ) • v ∈ interior s := by convert s_conv.add_smul_sub_mem_interior xs h4v A using 1 - simp only [smul_smul, one_div, add_sub_cancel_left, add_right_inj] - norm_num + module have h2w : x + (2 : ℝ) • w ∈ interior s := by convert s_conv.add_smul_sub_mem_interior xs h4w A using 1 - simp only [smul_smul, one_div, add_sub_cancel_left, add_right_inj] - norm_num + module have hvw : x + (v + w) ∈ interior s := by convert s_conv.add_smul_sub_mem_interior xs h2v2w A using 1 - simp only [smul_smul, one_div, add_sub_cancel_left, add_right_inj, smul_add, smul_sub] - norm_num - abel + module have h2vw : x + (2 • v + w) ∈ interior s := by convert s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1 - simp only [smul_add, smul_sub, smul_smul, ← C] - norm_num - abel + module have hvww : x + (v + w) + w ∈ interior s := by convert s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1 - rw [one_div, add_sub_add_right_eq_sub, add_sub_cancel_left, inv_smul_smul₀ two_ne_zero, - two_smul] - abel + module have TA1 := s_conv.taylor_approx_two_segment hf xs hx h2vw h2vww have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww convert TA1.sub TA2 using 1 @@ -245,11 +232,9 @@ theorem Convex.second_derivative_within_at_symmetric_of_mem_interior {v w : E} apply C.congr' _ _ · filter_upwards [self_mem_nhdsWithin] intro h (hpos : 0 < h) - rw [← one_smul ℝ (f'' w v - f'' v w), smul_smul, smul_smul] - congr 1 - field_simp [LT.lt.ne' hpos] + match_scalars <;> field_simp · filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h) - field_simp [LT.lt.ne' hpos, SMul.smul] + field_simp simpa only [sub_eq_zero] using isLittleO_const_const_iff.1 B end @@ -298,8 +283,8 @@ theorem Convex.second_derivative_within_at_symmetric {s : Set E} (s_conv : Conve s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts w) (ts v) simp only [ContinuousLinearMap.map_add, ContinuousLinearMap.map_smul, smul_add, smul_smul, ContinuousLinearMap.add_apply, Pi.smul_apply, ContinuousLinearMap.coe_smul', C] at this - rw [add_assoc, add_assoc, add_right_inj, add_left_comm, add_right_inj, add_right_inj, mul_comm] - at this + have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by + linear_combination (norm := module) this apply smul_right_injective F _ this simp [(tpos v).ne', (tpos w).ne'] diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean index df41e2606b7e8..434945a20c58c 100644 --- a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean +++ b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean @@ -356,8 +356,8 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l] apply ((this ε hε).filter_mono curry_le_prod).mono intro n hn rw [dist_eq_norm] at hn ⊢ - rw [← smul_sub] at hn - rwa [sub_zero] + convert hn using 2 + module · -- (Almost) the definition of the derivatives rw [Metric.tendsto_nhds] intro ε hε diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean index f07e88d57f245..1eb8cdb030baa 100644 --- a/Mathlib/Analysis/Convex/Basic.lean +++ b/Mathlib/Analysis/Convex/Basic.lean @@ -8,6 +8,8 @@ import Mathlib.Algebra.Order.Module.OrderedSMul import Mathlib.Algebra.Order.Module.Synonym import Mathlib.Analysis.Convex.Star import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.NoncommRing /-! # Convex sets and functions in vector spaces @@ -158,8 +160,7 @@ theorem convex_segment (x y : E) : Convex 𝕜 [x -[𝕜] y] := by ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq), add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩ · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab] - · simp_rw [add_smul, mul_smul, smul_add] - exact add_add_add_comm _ _ _ _ + · match_scalars <;> noncomm_ring theorem Convex.linear_image (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s) := by rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab @@ -406,8 +407,8 @@ theorem convex_openSegment (a b : E) : Convex 𝕜 (openSegment 𝕜 a b) := by rw [convex_iff_openSegment_subset] rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩ refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩ - · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab] - · simp_rw [add_smul, mul_smul, smul_add, add_add_add_comm] + · linear_combination (norm := noncomm_ring) a * habp + b * habq + hab + · module end StrictOrderedCommSemiring @@ -425,8 +426,7 @@ theorem convex_vadd (a : E) : Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s := theorem Convex.add_smul_mem (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s := by - have h : x + t • y = (1 - t) • x + t • (x + y) := by - rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul] + have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring rw [h] exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _) @@ -515,7 +515,7 @@ theorem Convex.exists_mem_add_smul_eq (h : Convex 𝕜 s) {x y : E} {p q : 𝕜} · replace hpq : 0 < p + q := (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq) refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩ - simp only [smul_add, smul_smul, mul_div_cancel₀ _ hpq.ne'] + match_scalars <;> field_simp theorem Convex.add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) : (p + q) • s = p • s + q • s := (add_smul_subset _ _ _).antisymm <| by diff --git a/Mathlib/Analysis/Convex/Combination.lean b/Mathlib/Analysis/Convex/Combination.lean index 1fc98bcd1e819..399464ada7406 100644 --- a/Mathlib/Analysis/Convex/Combination.lean +++ b/Mathlib/Analysis/Convex/Combination.lean @@ -50,7 +50,8 @@ theorem Finset.centerMass_empty : (∅ : Finset ι).centerMass w z = 0 := by theorem Finset.centerMass_pair (hne : i ≠ j) : ({i, j} : Finset ι).centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j := by - simp only [centerMass, sum_pair hne, smul_add, (mul_smul _ _ _).symm, div_eq_inv_mul] + simp only [centerMass, sum_pair hne] + module variable {w} @@ -63,7 +64,9 @@ theorem Finset.centerMass_insert (ha : i ∉ t) (hw : ∑ j ∈ t, w j ≠ 0) : rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div] theorem Finset.centerMass_singleton (hw : w i ≠ 0) : ({i} : Finset ι).centerMass w z = z i := by - rw [centerMass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel₀ hw, one_smul] + rw [centerMass, sum_singleton, sum_singleton] + match_scalars + field_simp @[simp] lemma Finset.centerMass_neg_left : t.centerMass (-w) z = t.centerMass w z := by simp [centerMass, inv_neg] diff --git a/Mathlib/Analysis/Convex/Jensen.lean b/Mathlib/Analysis/Convex/Jensen.lean index 20e5b017a492d..93f195e014393 100644 --- a/Mathlib/Analysis/Convex/Jensen.lean +++ b/Mathlib/Analysis/Convex/Jensen.lean @@ -118,11 +118,10 @@ lemma StrictConvexOn.map_sum_lt (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ have := h₀ k <| by simp let c := w j + w k have hc : w j / c + w k / c = 1 := by field_simp - have hcj : c * (w j / c) = w j := by field_simp - have hck : c * (w k / c) = w k := by field_simp calc f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x)) _ = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x) := by - rw [smul_add, ← mul_smul, ← mul_smul, hcj, hck, add_assoc] + congrm f ?_ + match_scalars <;> field_simp _ ≤ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) := -- apply the usual Jensen's inequality wrt the weighted average of the two distinguished -- points and all the other points @@ -134,7 +133,7 @@ lemma StrictConvexOn.map_sum_lt (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ -- then apply the definition of strict convexity for the two distinguished points gcongr; refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc <;> positivity _ = (w j • f (p j) + w k • f (p k)) + ∑ x ∈ u, w x • f (p x) := by - rw [smul_add, ← mul_smul, ← mul_smul, hcj, hck] + match_scalars <;> field_simp _ = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x)) := by abel_nf /-- Concave **strict Jensen inequality**. diff --git a/Mathlib/Analysis/Convex/Join.lean b/Mathlib/Analysis/Convex/Join.lean index a8641487cfccd..590ebaa4aa614 100644 --- a/Mathlib/Analysis/Convex/Join.lean +++ b/Mathlib/Analysis/Convex/Join.lean @@ -113,19 +113,13 @@ theorem convexJoin_assoc_aux (s t u : Set E) : rintro _ ⟨z, ⟨x, hx, y, hy, a₁, b₁, ha₁, hb₁, hab₁, rfl⟩, z, hz, a₂, b₂, ha₂, hb₂, hab₂, rfl⟩ obtain rfl | hb₂ := hb₂.eq_or_lt · refine ⟨x, hx, y, ⟨y, hy, z, hz, left_mem_segment 𝕜 _ _⟩, a₁, b₁, ha₁, hb₁, hab₁, ?_⟩ - rw [add_zero] at hab₂ - rw [hab₂, one_smul, zero_smul, add_zero] - have ha₂b₁ : 0 ≤ a₂ * b₁ := mul_nonneg ha₂ hb₁ - have hab : 0 < a₂ * b₁ + b₂ := add_pos_of_nonneg_of_pos ha₂b₁ hb₂ + linear_combination (norm := module) congr(-$hab₂ • (a₁ • x + b₁ • y)) refine ⟨x, hx, (a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z, - ⟨y, hy, z, hz, _, _, ?_, ?_, ?_, rfl⟩, - a₂ * a₁, a₂ * b₁ + b₂, mul_nonneg ha₂ ha₁, hab.le, ?_, ?_⟩ - · exact div_nonneg ha₂b₁ hab.le - · exact div_nonneg hb₂.le hab.le - · rw [← add_div, div_self hab.ne'] - · rw [← add_assoc, ← mul_add, hab₁, mul_one, hab₂] - · simp_rw [smul_add, ← mul_smul, mul_div_cancel₀ _ hab.ne', add_assoc] + ⟨y, hy, z, hz, _, _, by positivity, by positivity, by field_simp, rfl⟩, + a₂ * a₁, a₂ * b₁ + b₂, by positivity, by positivity, ?_, ?_⟩ + · linear_combination a₂ * hab₁ + hab₂ + · match_scalars <;> field_simp theorem convexJoin_assoc (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u) := by @@ -155,9 +149,9 @@ protected theorem Convex.convexJoin (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : rcases hs.exists_mem_add_smul_eq hx₁ hx₂ (mul_nonneg hp ha₁) (mul_nonneg hq ha₂) with ⟨x, hxs, hx⟩ rcases ht.exists_mem_add_smul_eq hy₁ hy₂ (mul_nonneg hp hb₁) (mul_nonneg hq hb₂) with ⟨y, hyt, hy⟩ refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩ <;> try positivity - · rwa [add_add_add_comm, ← mul_add, ← mul_add, hab₁, hab₂, mul_one, mul_one] - · rw [hx, hy, add_add_add_comm] - simp only [smul_add, smul_smul] + · linear_combination p * hab₁ + q * hab₂ + hpq + · rw [hx, hy] + module protected theorem Convex.convexHull_union (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hs₀ : s.Nonempty) (ht₀ : t.Nonempty) : convexHull 𝕜 (s ∪ t) = convexJoin 𝕜 s t := diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean index 4bedc05dc363e..f4c36915e34ea 100644 --- a/Mathlib/Analysis/Convex/Side.lean +++ b/Mathlib/Analysis/Convex/Side.lean @@ -333,12 +333,8 @@ theorem _root_.Wbtw.wOppSide₁₃ {s : AffineSubspace R P} {x y z : P} (h : Wbt rcases ht0.lt_or_eq with (ht0' | rfl); swap · rw [lineMap_apply_zero]; simp refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩) - -- TODO: after lean4#2336 "simp made no progress feature" - -- had to add `_` to several lemmas here. Not sure why! - simp_rw [lineMap_apply _, vadd_vsub_assoc _, vsub_vadd_eq_vsub_sub _, - ← neg_vsub_eq_vsub_rev z x, vsub_self _, zero_sub, ← neg_one_smul R (z -ᵥ x), - ← add_smul, smul_neg, ← neg_smul, smul_smul] - ring_nf + rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z, vsub_self] + module theorem _root_.Wbtw.wOppSide₃₁ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hy : y ∈ s) : s.WOppSide z x := @@ -411,9 +407,9 @@ theorem wOppSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p exact SameRay.zero_right _ · refine Or.inr ⟨(-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂', Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩ - rw [vadd_vsub_assoc, smul_add, ← hr, smul_smul, neg_div, mul_neg, - mul_div_cancel₀ _ hr₂.ne.symm, neg_smul, neg_add_eq_sub, ← smul_sub, - vsub_sub_vsub_cancel_right] + rw [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁'] + linear_combination (norm := match_scalars <;> field_simp) hr + ring · rintro (h' | ⟨h₁, h₂, h₃⟩) · exact wOppSide_of_left_mem y h' · exact ⟨p₁, h, h₁, h₂, h₃⟩ @@ -584,15 +580,14 @@ theorem wOppSide_iff_exists_wbtw {s : AffineSubspace R P} {x y : P} : · refine ⟨lineMap x y (r₂ / (r₁ + r₂)), ?_, ?_⟩ · have : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) := by - rw [add_comm (y -ᵥ p₂), smul_sub, smul_add, add_sub_assoc, add_assoc, add_right_eq_self, - div_eq_inv_mul, ← neg_vsub_eq_vsub_rev, smul_neg, ← smul_smul, ← h, smul_smul, ← neg_smul, - ← sub_smul, ← div_eq_inv_mul, ← div_eq_inv_mul, ← neg_div, ← sub_div, sub_eq_add_neg, - ← neg_add, neg_div, div_self (Left.add_pos hr₁ hr₂).ne.symm, neg_one_smul, neg_add_cancel] + rw [← neg_vsub_eq_vsub_rev p₂ y] + linear_combination (norm := match_scalars <;> field_simp) congr((r₁ + r₂)⁻¹ • $h) + ring rw [lineMap_apply, ← vsub_vadd x p₁, ← vsub_vadd y p₂, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, ← vadd_assoc, vadd_eq_add, this] exact s.smul_vsub_vadd_mem (r₂ / (r₁ + r₂)) hp₂ hp₁ hp₁ · exact Set.mem_image_of_mem _ - ⟨div_nonneg hr₂.le (Left.add_pos hr₁ hr₂).le, + ⟨by positivity, div_le_one_of_le (le_add_of_nonneg_left hr₁.le) (Left.add_pos hr₁ hr₂).le⟩ theorem SOppSide.exists_sbtw {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : diff --git a/Mathlib/Analysis/Convex/Star.lean b/Mathlib/Analysis/Convex/Star.lean index 44f1a60ccabfb..35d31a5d32be1 100644 --- a/Mathlib/Analysis/Convex/Star.lean +++ b/Mathlib/Analysis/Convex/Star.lean @@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.Module.Synonym import Mathlib.Algebra.Order.Group.Instances import Mathlib.Analysis.Convex.Segment import Mathlib.Tactic.GCongr +import Mathlib.Tactic.Module /-! # Star-convex sets @@ -210,14 +211,14 @@ theorem StarConvex.add_left (hs : StarConvex 𝕜 x s) (z : E) : intro y hy a b ha hb hab obtain ⟨y', hy', rfl⟩ := hy refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩ - rw [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] + match_scalars <;> simp [hab] theorem StarConvex.add_right (hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (x + z) ((fun x => x + z) '' s) := by intro y hy a b ha hb hab obtain ⟨y', hy', rfl⟩ := hy refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩ - rw [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] + match_scalars <;> simp [hab] /-- The translation of a star-convex set is also star-convex. -/ theorem StarConvex.preimage_add_right (hs : StarConvex 𝕜 (z + x) s) : diff --git a/Mathlib/Analysis/Convex/StoneSeparation.lean b/Mathlib/Analysis/Convex/StoneSeparation.lean index 4f746cd1909fd..1027690d2b881 100644 --- a/Mathlib/Analysis/Convex/StoneSeparation.lean +++ b/Mathlib/Analysis/Convex/StoneSeparation.lean @@ -46,9 +46,6 @@ theorem not_disjoint_segment_convexHull_triple {p q u v x y z : E} (hz : z ∈ s · positivity · positivity · rw [← add_div, div_self]; positivity - rw [smul_add, smul_add, add_add_add_comm] - nth_rw 2 [add_comm] - rw [← mul_smul, ← mul_smul] classical let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av] let z : Fin 3 → E := ![p, q, az • x + bz • y] @@ -61,18 +58,15 @@ theorem not_disjoint_segment_convexHull_triple {p q u v x y z : E} (hz : z ∈ s have hw : ∑ i, w i = az * av + bz * au := by trans az * av * bu + (bz * au * bv + au * av) · simp [w, Fin.sum_univ_succ, Fin.sum_univ_zero] - rw [← one_mul (au * av), ← habz, add_mul, ← add_assoc, add_add_add_comm, mul_assoc, ← mul_add, - mul_assoc, ← mul_add, mul_comm av, ← add_mul, ← mul_add, add_comm bu, add_comm bv, habu, - habv, one_mul, mul_one] + linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z] convert (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i) (by rwa [hw]) fun i _ => hz i : Finset.univ.centerMass w z ∈ _) - rw [Finset.centerMass] - simp_rw [div_eq_inv_mul, hw, mul_assoc, mul_smul (az * av + bz * au)⁻¹, ← smul_add, add_assoc, ← - mul_assoc] + rw [Finset.centerMass, hw] + trans (az * av + bz * au)⁻¹ • + ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y))) + · module congr 3 - rw [← mul_smul, ← mul_rotate, mul_right_comm, mul_smul, ← mul_smul _ av, mul_rotate, - mul_smul _ bz, ← smul_add] simp only [w, z, smul_add, List.foldr, Matrix.cons_val_succ', Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, add_zero] diff --git a/Mathlib/Analysis/Convex/Strict.lean b/Mathlib/Analysis/Convex/Strict.lean index da771a82ffc55..43a8732b0e6d3 100644 --- a/Mathlib/Analysis/Convex/Strict.lean +++ b/Mathlib/Analysis/Convex/Strict.lean @@ -302,8 +302,7 @@ theorem StrictConvex.eq_of_openSegment_subset_frontier [Nontrivial 𝕜] [Densel theorem StrictConvex.add_smul_mem (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s) (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • y ∈ interior s := by - have h : x + t • y = (1 - t) • x + t • (x + y) := by - rw [smul_add, ← add_assoc, ← _root_.add_smul, sub_add_cancel, one_smul] + have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> field_simp rw [h] exact hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero])) (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel 1 t) @@ -359,16 +358,14 @@ theorem strictConvex_iff_div : StrictConvex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s := - ⟨fun h x hx y hy hxy a b ha hb => by - apply h hx hy hxy (div_pos ha <| add_pos ha hb) (div_pos hb <| add_pos ha hb) - rw [← add_div] - exact div_self (add_pos ha hb).ne', fun h x hx y hy hxy a b ha hb hab => by + ⟨fun h x hx y hy hxy a b ha hb ↦ h hx hy hxy (by positivity) (by positivity) (by field_simp), + fun h x hx y hy hxy a b ha hb hab ↦ by convert h hx hy hxy ha hb <;> rw [hab, div_one]⟩ theorem StrictConvex.mem_smul_of_zero_mem (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) : x ∈ t • interior s := by - rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans ht).ne'] - exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (inv_pos.2 <| zero_lt_one.trans ht) (inv_lt_one ht) + rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)] + exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one ht) end AddCommGroup diff --git a/Mathlib/Analysis/NormedSpace/Connected.lean b/Mathlib/Analysis/NormedSpace/Connected.lean index 64d98223dda5e..e14389a41de74 100644 --- a/Mathlib/Analysis/NormedSpace/Connected.lean +++ b/Mathlib/Analysis/NormedSpace/Connected.lean @@ -52,13 +52,11 @@ theorem Set.Countable.isPathConnected_compl_of_one_lt_rank let c := (2 : ℝ)⁻¹ • (a + b) let x := (2 : ℝ)⁻¹ • (b - a) have Ia : c - x = a := by - simp only [c, x, smul_add, smul_sub] - abel_nf - simp [← Int.cast_smul_eq_zsmul ℝ 2] + simp only [c, x] + module have Ib : c + x = b := by - simp only [c, x, smul_add, smul_sub] - abel_nf - simp [← Int.cast_smul_eq_zsmul ℝ 2] + simp only [c, x] + module have x_ne_zero : x ≠ 0 := by simpa [x] using sub_ne_zero.2 hab.symm obtain ⟨y, hy⟩ : ∃ y, LinearIndependent ℝ ![x, y] := exists_linearIndependent_pair_of_one_lt_rank h x_ne_zero diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean index b933762e6b4a6..7f40cc129de8e 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean @@ -65,9 +65,8 @@ def rotation (θ : Real.Angle) : V ≃ₗᵢ[ℝ] V := · simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap, LinearIsometryEquiv.coe_toLinearEquiv, map_smul, map_sub, LinearMap.coe_comp, - LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply, ← mul_smul, add_smul, - smul_add, smul_neg, smul_sub, mul_comm, sq] - abel + LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply] + module · simp) (by ext x @@ -75,10 +74,8 @@ def rotation (θ : Real.Angle) : V ≃ₗᵢ[ℝ] V := · simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap, LinearIsometryEquiv.coe_toLinearEquiv, map_add, map_smul, LinearMap.coe_comp, - LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply, - add_smul, smul_neg, smul_sub, smul_smul] - ring_nf - abel + LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply] + module · simp) theorem rotation_apply (θ : Real.Angle) (x : V) : @@ -146,11 +143,9 @@ theorem rotation_pi_div_two : o.rotation (π / 2 : ℝ) = J := by @[simp] theorem rotation_rotation (θ₁ θ₂ : Real.Angle) (x : V) : o.rotation θ₁ (o.rotation θ₂ x) = o.rotation (θ₁ + θ₂) x := by - simp only [o.rotation_apply, ← mul_smul, Real.Angle.cos_add, Real.Angle.sin_add, add_smul, - sub_smul, LinearIsometryEquiv.trans_apply, smul_add, LinearIsometryEquiv.map_add, - LinearIsometryEquiv.map_smul, rightAngleRotation_rightAngleRotation, smul_neg] - ring_nf - abel + simp only [o.rotation_apply, Real.Angle.cos_add, Real.Angle.sin_add, LinearIsometryEquiv.map_add, + LinearIsometryEquiv.trans_apply, map_smul, rightAngleRotation_rightAngleRotation] + module /-- Rotating twice is equivalent to rotating by the sum of the angles. -/ @[simp] diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index ed68d3b7b7e44..f045983a13cd3 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -11,7 +11,8 @@ import Mathlib.Tactic.FinCases import Mathlib.Tactic.LinearCombination import Mathlib.Lean.Expr.ExtraRecognizers import Mathlib.Data.Set.Subsingleton -import Mathlib.Tactic.Abel +import Mathlib.Tactic.Module +import Mathlib.Tactic.NoncommRing /-! @@ -596,9 +597,8 @@ theorem LinearIndependent.units_smul {v : ι → M} (hv : LinearIndependent R v) lemma LinearIndependent.eq_of_pair {x y : M} (h : LinearIndependent R ![x, y]) {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) : s = s' ∧ t = t' := by have : (s - s') • x + (t - t') • y = 0 := by - rw [← sub_eq_zero_of_eq h', ← sub_eq_zero] - simp only [sub_smul] - abel + rw [← sub_eq_zero_of_eq h'] + match_scalars <;> noncomm_ring simpa [sub_eq_zero] using h.eq_zero_of_pair this lemma LinearIndependent.eq_zero_of_pair' {x y : M} (h : LinearIndependent R ![x, y]) @@ -616,8 +616,7 @@ lemma LinearIndependent.linear_combination_pair_of_det_ne_zero {R M : Type*} [Co apply LinearIndependent.pair_iff.2 (fun s t hst ↦ ?_) have H : (s * a + t * c) • x + (s * b + t * d) • y = 0 := by convert hst using 1 - simp only [_root_.add_smul, smul_add, smul_smul] - abel + module have I1 : s * a + t * c = 0 := (h.eq_zero_of_pair H).1 have I2 : s * b + t * d = 0 := (h.eq_zero_of_pair H).2 have J1 : (a * d - b * c) * s = 0 := by linear_combination d * I1 - c * I2 @@ -1111,11 +1110,10 @@ theorem linearIndependent_monoidHom (G : Type*) [Monoid G] (L : Type*) [CommRing rw [Finset.sum_insert has, Finset.sum_insert has] _ = (∑ i ∈ insert a s, g i * i (x * y)) - - ∑ i ∈ insert a s, a x * (g i * i y) := - congr - (congr_arg Sub.sub - (Finset.sum_congr rfl fun i _ => by rw [i.map_mul, mul_assoc])) - (Finset.sum_congr rfl fun _ _ => by rw [mul_assoc, mul_left_comm]) + ∑ i ∈ insert a s, a x * (g i * i y) := by + congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_ + · rw [map_mul, mul_assoc] + · rw [mul_assoc, mul_left_comm] _ = (∑ i ∈ insert a s, (g i • (i : G → L))) (x * y) - a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by @@ -1231,7 +1229,7 @@ theorem mem_span_insert_exchange : have a0 : a ≠ 0 := by rintro rfl simp_all - simp [a0, smul_add, smul_smul] + match_scalars <;> simp [a0] theorem linearIndependent_iff_not_mem_span : LinearIndependent K v ↔ ∀ i, v i ∉ span K (v '' (univ \ {i})) := by @@ -1305,8 +1303,8 @@ theorem LinearIndependent.pair_iff' {x y : V} (hx : x ≠ 0) : by_cases ht : t = 0 · exact ⟨by simpa [ht, hx] using hst, ht⟩ apply_fun (t⁻¹ • ·) at hst - simp only [smul_add, smul_smul, inv_mul_cancel₀ ht, one_smul, smul_zero] at hst - cases H (-(t⁻¹ * s)) (by rwa [neg_smul, neg_eq_iff_eq_neg, eq_neg_iff_add_eq_zero]) + simp only [smul_add, smul_smul, inv_mul_cancel₀ ht] at hst + cases H (-(t⁻¹ * s)) <| by linear_combination (norm := match_scalars <;> noncomm_ring) -hst theorem linearIndependent_fin_cons {n} {v : Fin n → V} : LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) ↔ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index caedda89e57e7..7eba713353773 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -854,15 +854,15 @@ theorem associated_toQuadraticMap (B : BilinMap R M R) (x y : M) : theorem associated_left_inverse (h : B₁.IsSymm) : associatedHom S B₁.toQuadraticMap = B₁ := LinearMap.ext₂ fun x y => by - rw [associated_toQuadraticMap, ← h.eq x y, RingHom.id_apply, ← two_mul, ← smul_mul_assoc, - smul_eq_mul, invOf_mul_self, one_mul] + rw [associated_toQuadraticMap, ← h.eq x y, RingHom.id_apply] + match_scalars + linear_combination invOf_mul_self' (2:R) -- Porting note: moved from below to golf the next theorem theorem associated_eq_self_apply (x : M) : associatedHom S Q x x = Q x := by - rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul, - add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R, - ← smul_assoc] - simp only [smul_eq_mul, invOf_mul_self', one_smul] + rw [associated_apply, map_add_self] + match_scalars + linear_combination invOf_mul_self' (2:R) theorem toQuadraticMap_associated : (associatedHom S Q).toQuadraticMap = Q := QuadraticMap.ext <| associated_eq_self_apply S Q @@ -1288,8 +1288,7 @@ theorem basisRepr_eq_of_iIsOrtho {R M} [CommRing R] [AddCommGroup M] [Module R M smul_eq_mul, smul_eq_mul] ring_nf · intro i _ hij - rw [LinearMap.map_smul, LinearMap.map_smul₂, - show associatedHom R Q (v i) (v j) = 0 from hv₂ hij, smul_eq_mul, smul_eq_mul, - mul_zero, mul_zero] + rw [LinearMap.map_smul, LinearMap.map_smul₂, hv₂ hij] + module end QuadraticMap diff --git a/Mathlib/LinearAlgebra/Ray.lean b/Mathlib/LinearAlgebra/Ray.lean index 87778718498eb..547a7c8540f4b 100644 --- a/Mathlib/LinearAlgebra/Ray.lean +++ b/Mathlib/LinearAlgebra/Ray.lean @@ -6,6 +6,7 @@ Authors: Joseph Myers import Mathlib.Algebra.Order.Module.Algebra import Mathlib.LinearAlgebra.LinearIndependent import Mathlib.Algebra.Ring.Subring.Units +import Mathlib.Tactic.Positivity /-! # Rays in modules @@ -106,7 +107,7 @@ lemma sameRay_nonneg_smul_right (v : M) (h : 0 ≤ a) : SameRay R v (a • v) := · rw [← algebraMap_smul R a v, h, zero_smul] exact zero_right _ · refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩ - rw [algebraMap_smul, one_smul] + module /-- A nonnegative multiple of a vector is in the same ray as that vector. -/ lemma sameRay_nonneg_smul_left (v : M) (ha : 0 ≤ a) : SameRay R (a • v) v := @@ -170,9 +171,8 @@ theorem add_left (hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩ rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩ refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩) - · apply_rules [add_pos, mul_pos] - · simp only [mul_smul, smul_add, add_smul, ← Hx, ← Hy] - rw [smul_comm] + · positivity + · convert congr(ry • $Hx + rx • $Hy) using 1 <;> module /-- If `y` and `z` are on the same ray as `x`, then so is `y + z`. -/ theorem add_right (hy : SameRay R x y) (hz : SameRay R x z) : SameRay R x (y + z) := @@ -531,11 +531,11 @@ theorem sameRay_or_sameRay_neg_iff_not_linearIndependent {x y : M} : rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1) · refine Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩)) - rw [neg_smul_neg, neg_smul, hm, neg_neg] + linear_combination (norm := module) -hm · exfalso simp [hm1, hx, hm0.ne] at hm · refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩)) - rw [neg_smul, hm, neg_neg] + linear_combination (norm := module) -hm · exfalso simp [hm0, hy, hm1.ne] at hm · rw [Fin.exists_fin_two] at hmne diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean index df6dd1f46c15f..6c8bfa2572edc 100644 --- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean +++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean @@ -427,10 +427,8 @@ theorem functional_equation₀ (s : ℂ) : P.Λ₀ (P.k - s) = P.ε • P.symm. /-- Functional equation formulated for `Λ`. -/ theorem functional_equation (s : ℂ) : P.Λ (P.k - s) = P.ε • P.symm.Λ s := by - have := P.functional_equation₀ s - rw [P.Λ₀_eq, P.symm_Λ₀_eq, sub_sub_cancel] at this - rwa [smul_add, smul_add, ← mul_smul, mul_one_div, ← mul_smul, ← mul_div_assoc, - mul_inv_cancel₀ P.hε, add_assoc, add_comm (_ • _), add_assoc, add_left_inj] at this + linear_combination (norm := module) P.functional_equation₀ s - P.Λ₀_eq (P.k - s) + + congr(P.ε • $(P.symm_Λ₀_eq s)) + congr(($(mul_inv_cancel₀ P.hε) / ((P.k:ℂ) - s)) • P.f₀) /-- The residue of `Λ` at `s = k` is equal to `ε • g₀`. -/ theorem Λ_residue_k : @@ -444,8 +442,7 @@ theorem Λ_residue_k : exact continuousAt_const.div continuousAt_id (ofReal_ne_zero.mpr P.hk.ne') · refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_ refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ P.k) ↦ ?_) - simp_rw [← mul_smul] - congr 1 + match_scalars field_simp [sub_ne_zero.mpr hs.symm] ring @@ -457,7 +454,7 @@ theorem Λ_residue_zero : · exact (continuous_id.smul P.differentiable_Λ₀.continuous).tendsto _ · refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_ refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ 0) ↦ ?_) - simp_rw [← mul_smul] + match_scalars field_simp [sub_ne_zero.mpr hs.symm] · rw [show 𝓝 0 = 𝓝 ((0 : ℂ) • (P.ε / (P.k - 0 : ℂ)) • P.g₀) by rw [zero_smul]] exact (continuousAt_id.smul ((continuousAt_const.div ((continuous_sub_left _).continuousAt)