From f7022be9efd23a865c9bdd9ac8a35447dab327ff Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 12 May 2026 21:37:01 +0200 Subject: [PATCH 1/4] perf: increase some instance priorities --- Mathlib/Algebra/Ring/Defs.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean index 2c2a9eb9aecfb6..494bfa1013846c 100644 --- a/Mathlib/Algebra/Ring/Defs.lean +++ b/Mathlib/Algebra/Ring/Defs.lean @@ -145,6 +145,8 @@ class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, /-- A `Ring` is a `Semiring` with negation making it an additive group. -/ class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R +attribute [instance 1100] Ring.toSemiring + /-! ### Semirings -/ @@ -221,6 +223,8 @@ class NonAssocCommSemiring (α : Type u) /-- A commutative semiring is a semiring with commutative multiplication. -/ class CommSemiring (R : Type u) extends Semiring R, CommMonoid R +attribute [instance 1100] CommSemiring.toSemiring + attribute [instance 100] NonAssocCommSemiring.toNonAssocSemiring attribute [instance 100] NonAssocCommSemiring.toNonUnitalNonAssocCommSemiring @@ -405,6 +409,8 @@ instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUni /-- A commutative ring is a ring with commutative multiplication. -/ class CommRing (α : Type u) extends Ring α, CommMonoid α +attribute [instance 1100] CommRing.toRing + instance (priority := 100) CommRing.toNonAssocCommRing [CommRing α] : NonAssocCommRing α where instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α := From 86ce07359f73019dc71d25cb8ec625fd1e95d37d Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 12 May 2026 21:58:33 +0200 Subject: [PATCH 2/4] two fixes --- Mathlib/Algebra/Polynomial/Coeff.lean | 5 +++-- Mathlib/RingTheory/Finiteness/Basic.lean | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Coeff.lean b/Mathlib/Algebra/Polynomial/Coeff.lean index c8158f3421dbb4..f8c564825fca60 100644 --- a/Mathlib/Algebra/Polynomial/Coeff.lean +++ b/Mathlib/Algebra/Polynomial/Coeff.lean @@ -299,10 +299,11 @@ theorem coeff_X_add_C_pow (r : R) (n k : ℕ) : rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero] theorem coeff_X_add_one_pow (R : Type*) [Semiring R] (n k : ℕ) : - ((X + 1) ^ n).coeff k = (n.choose k : R) := by rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul] + ((X + 1 : R[X]) ^ n).coeff k = (n.choose k : R) := by + rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul] theorem coeff_one_add_X_pow (R : Type*) [Semiring R] (n k : ℕ) : - ((1 + X) ^ n).coeff k = (n.choose k : R) := by rw [add_comm _ X, coeff_X_add_one_pow] + ((1 + X : R[X]) ^ n).coeff k = (n.choose k : R) := by rw [add_comm _ X, coeff_X_add_one_pow] theorem one_add_X_pow_sub_X_pow {S : Type*} [CommRing S] (d : ℕ) : (1 + X : S[X]) ^ d - X ^ d = ∑ i ∈ range d, d.choose i • X ^ i := by diff --git a/Mathlib/RingTheory/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean index 1044b0ae92511e..cd36f5fc10ee52 100644 --- a/Mathlib/RingTheory/Finiteness/Basic.lean +++ b/Mathlib/RingTheory/Finiteness/Basic.lean @@ -343,8 +343,9 @@ instance bot : Module.Finite R (⊥ : Submodule R M) := .of_fg fg_bot instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := .of_fg fg_top instance top_left [Module.Finite R M] : Module.Finite (⊤ : Subsemiring R) M := - have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom := - RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm + have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom := { + is_surjective := Function.RightInverse.surjective (congrFun rfl) + } -- RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm of_surjective (σ := (Subsemiring.topEquiv (R := R)).symm.toRingHom) ⟨⟨id, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩ Function.surjective_id From 387ebdbc0ac2c0a7c24525c31ad1ad0134d23df8 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 12 May 2026 22:04:07 +0200 Subject: [PATCH 3/4] two more fixes --- Mathlib/Algebra/Polynomial/Eval/Degree.lean | 2 +- Mathlib/Data/Nat/Choose/Vandermonde.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Eval/Degree.lean b/Mathlib/Algebra/Polynomial/Eval/Degree.lean index 0ea93154dbfed2..f24a9d76d5c707 100644 --- a/Mathlib/Algebra/Polynomial/Eval/Degree.lean +++ b/Mathlib/Algebra/Polynomial/Eval/Degree.lean @@ -106,7 +106,7 @@ theorem coeff_comp_degree_mul_degree (hqd0 : natDegree q ≠ 0) : @[simp] lemma comp_C_mul_X_coeff {r : R} {n : ℕ} : (p.comp <| C r * X).coeff n = p.coeff n * r ^ n := by - simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow, + simp_rw [comp, eval₂_eq_sum_range, (commute_X (R := R) _).symm.mul_pow, ← C_pow, finsetSum_coeff, coeff_C_mul, coeff_X_pow] rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one] · intro b _ h; simp_rw [if_neg h.symm, mul_zero] diff --git a/Mathlib/Data/Nat/Choose/Vandermonde.lean b/Mathlib/Data/Nat/Choose/Vandermonde.lean index 771eb08dd0cd10..77a11583103105 100644 --- a/Mathlib/Data/Nat/Choose/Vandermonde.lean +++ b/Mathlib/Data/Nat/Choose/Vandermonde.lean @@ -31,8 +31,8 @@ namespace Nat theorem add_choose_eq (m n k : ℕ) : (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by calc - (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id] - _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add] + (m + n).choose k = ((X + 1 : ℕ[X]) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id] + _ = ((X + 1) ^ m * (X + 1 : ℕ[X]) ^ n).coeff k := by rw [pow_add] _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by rw [coeff_mul, Finset.sum_congr rfl] simp only [coeff_X_add_one_pow, cast_id, imp_true_iff] From f6731f2dc73d8cdb0c11ffa3f7030879807f92bf Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Tue, 12 May 2026 23:41:40 +0200 Subject: [PATCH 4/4] more fixes (one sorry left) --- Mathlib/Algebra/Polynomial/Bivariate.lean | 2 +- Mathlib/Algebra/Quaternion.lean | 1 + Mathlib/Analysis/Calculus/FDeriv/Add.lean | 12 ++++++++---- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean | 10 ++++++---- Mathlib/FieldTheory/SeparableClosure.lean | 1 + .../RingTheory/Extension/Cotangent/BaseChange.lean | 4 +++- Mathlib/RingTheory/Polynomial/IsIntegral.lean | 4 +++- .../Spectrum/Prime/ChevalleyComplexity.lean | 3 +++ Mathlib/Topology/Algebra/Polynomial.lean | 3 ++- 9 files changed, 28 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Bivariate.lean b/Mathlib/Algebra/Polynomial/Bivariate.lean index f4259883ab255c..ccaa74e4cbc6b2 100644 --- a/Mathlib/Algebra/Polynomial/Bivariate.lean +++ b/Mathlib/Algebra/Polynomial/Bivariate.lean @@ -280,7 +280,7 @@ theorem Bivariate.swap_monomial (n : ℕ) (f : R[X]) : theorem Bivariate.swap_monomial_monomial (n m : ℕ) (r : R) : swap (monomial n (monomial m r)) = (monomial m (monomial n r)) := by - simp [← C_mul_X_pow_eq_monomial]; ac_rfl + simp [← C_mul_X_pow_eq_monomial, X_pow_mul_assoc] /-- Evaluating `swap p` at `x`, `y` is the same as evaluating `p` at `y` `x`. -/ theorem Bivariate.aevalAeval_swap (x y : A) (p : R[X][Y]) : diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index 45ac70fdc75648..0a1dd2ae8aca5a 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -1217,6 +1217,7 @@ theorem normSq_div : normSq (a / b) = normSq a / normSq b := theorem normSq_zpow (z : ℤ) : normSq (a ^ z) = normSq a ^ z := map_zpow₀ normSq a z +omit [LinearOrder R] [IsStrictOrderedRing R] in @[norm_cast] theorem normSq_ratCast (q : ℚ) : normSq (q : ℍ[R]) = (q : ℍ[R]) ^ 2 := by rw [← coe_ratCast, normSq_coe, coe_pow] diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean index 87d70486e27ee5..40b176f11a2054 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean @@ -133,7 +133,7 @@ lemma differentiableAt_smul_iff (c : R) [Invertible c] : `c` must be invertible, i.e. if `R` is a field. -/ theorem fderiv_const_smul_of_invertible (c : R) [Invertible c] : fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x := by - simp [← fderivWithin_univ, fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ] + simpa [← fderivWithin_univ] using fderivWithin_const_smul_of_invertible c uniqueDiffWithinAt_univ end ConstSMul @@ -178,7 +178,9 @@ typeclass. -/ lemma fderiv_const_smul_field (c : R) : fderiv 𝕜 (c • f) = c • fderiv 𝕜 f := by simp_rw [← fderivWithin_univ] ext x - simp [fderivWithin_const_smul_field c uniqueDiffWithinAt_univ] + simp only [Pi.smul_apply, coe_smul'] + rw [fderivWithin_const_smul_field c uniqueDiffWithinAt_univ] + exact smul_apply c (fderivWithin 𝕜 f Set.univ x) _ @[deprecated (since := "2026-01-11")] alias fderiv_const_smul_of_field := fderiv_const_smul_field @@ -595,7 +597,8 @@ theorem fderivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) : @[simp] theorem fderiv_fun_neg : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x := by - simp only [← fderivWithin_univ, fderivWithin_fun_neg uniqueDiffWithinAt_univ] + simp only [← fderivWithin_univ] + rw [fderivWithin_fun_neg uniqueDiffWithinAt_univ] /-- Version of `fderiv_neg` where the function is written `-f` instead of `fun y ↦ - f y`. -/ theorem fderiv_neg : fderiv 𝕜 (-f) x = -fderiv 𝕜 f x := @@ -842,7 +845,8 @@ theorem fderivWithin_const_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (c : F) : simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_fun_neg, hxs] theorem fderiv_const_sub (c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x := by - simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ] + simp only [← fderivWithin_univ] + rw [fderivWithin_const_sub uniqueDiffWithinAt_univ] end Sub diff --git a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean index a4a522ec102b64..234cfe0dad10b8 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean @@ -124,7 +124,8 @@ theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X] /-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/ theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by - simpa only [eval_X_pow, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X]) + have := subset_polynomial_aeval a (X ^ n : 𝕜[X]) + simpa only [eval_X_pow, aeval_X_pow] using this theorem pow_mem_pow (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ σ a) : k ^ n ∈ σ (a ^ n) := pow_image_subset a n ⟨k, ⟨hk, rfl⟩⟩ @@ -133,14 +134,15 @@ theorem pow_mem_pow (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ σ a) : k ^ n ∈ convenience. -/ theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) : σ (a ^ n) = (· ^ n) '' σ a := by - simpa only [aeval_X_pow, eval_X_pow] - using map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos]) + have := map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos]) + simpa only [aeval_X_pow, eval_X_pow] using this /-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for convenience. -/ theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) : σ (a ^ n) = (· ^ n) '' σ a := by - simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval_of_nonempty a (X ^ n) ha + have := map_polynomial_aeval_of_nonempty a (X ^ n) ha + simpa only [aeval_X_pow, eval_X_pow] using this variable (𝕜) diff --git a/Mathlib/FieldTheory/SeparableClosure.lean b/Mathlib/FieldTheory/SeparableClosure.lean index 6f019bf2a03a7d..97c9ed1207c3f4 100644 --- a/Mathlib/FieldTheory/SeparableClosure.lean +++ b/Mathlib/FieldTheory/SeparableClosure.lean @@ -398,6 +398,7 @@ lemma exists_finset_maximalFor_isTranscendenceBasis_separableClosure · convert hs.isAlgebraic_field <;> simp [s] have : Module.Finite ((separableClosure (adjoin F (s : Set E)) E).restrictScalars F) E := inferInstanceAs <| Module.Finite (separableClosure (adjoin F (s : Set E)) E) E + stop exact d.not_lt_argminOn _ ht (by apply finrank_lt_of_gt H) @[deprecated (since := "2025-12-08")] diff --git a/Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean b/Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean index 04fd2e26e6b62c..8a2aa28a531a0e 100644 --- a/Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean +++ b/Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean @@ -101,6 +101,8 @@ lemma tensorCotangentSpace_tmul (t : T) (x : P.CotangentSpace) : simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map, smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra] +-- #defeq_abuse in +set_option backward.isDefEq.respectTransparency false in /-- If `T` is flat over `R`, there is a `T`-linear isomorphism `T ⊗[R] P.Cotangent ≃ₗ[T] (P.baseChange).Cotangent`. -/ noncomputable def tensorCotangentOfFlat [Module.Flat R T] : @@ -118,7 +120,7 @@ lemma tensorCotangentOfFlat_tmul [Module.Flat R T] (t : T) (x : P.Cotangent) : simp only [tensorCotangentOfFlat, LinearEquiv.trans_apply, AlgebraTensorModule.congr_tmul, LinearEquiv.refl_apply, LinearEquiv.restrictScalars_apply, cotangentEquivCotangentKer_apply, Cotangent.val_mk, Ideal.tensorCotangentEquiv_tmul, map_smul, Cotangent.map_mk, - Hom.toAlgHom_apply, Ideal.Cotangent.equivOfEq_toCotangent] + Hom.toAlgHom_apply] --, Ideal.Cotangent.equivOfEq_toCotangent] rfl /-- The canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange).H1Cotangent`. -/ diff --git a/Mathlib/RingTheory/Polynomial/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/IsIntegral.lean index cbf2125c6bc6a3..6c63265edaf57b 100644 --- a/Mathlib/RingTheory/Polynomial/IsIntegral.lean +++ b/Mathlib/RingTheory/Polynomial/IsIntegral.lean @@ -215,7 +215,9 @@ theorem MvPolynomial.isIntegral_iff_isIntegral_coeff.{w} {σ : Type w} {f : MvPo convert H.map ((rename Subtype.val).comp (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom · exact RingHom.ext (by simp [MvPolynomial.killCompl_map]) - · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _) + · conv_lhs => rw [← hg] + conv_rhs => enter [2]; rw [← hg] + simp)) n (.of_fintype _) · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)] exact isIntegral_zero revert f n diff --git a/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean b/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean index 72ba82d2dbecce..d8a7782b16c5d6 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean @@ -272,6 +272,9 @@ private lemma induction_structure (n : ℕ) Ideal.Quotient.mk_singleton_self, ne_eq, not_true_eq_false, false_or] at h_eq exact hi h_eq +attribute [local instance 1000] Ring.toSemiring +attribute [local instance 1000] CommSemiring.toSemiring + -- TODO: fix non-terminal simp (large simp set) set_option linter.flexible false in open IsLocalization in diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean index 0081a69f310193..06be4a7e06fa9a 100644 --- a/Mathlib/Topology/Algebra/Polynomial.lean +++ b/Mathlib/Topology/Algebra/Polynomial.lean @@ -151,7 +151,8 @@ theorem isClosedMap_eval [ProperSpace R] (p : R[X]) : IsClosedMap p.eval := by variable (R) in theorem _root_.isClosedMap_pow [ProperSpace R] (n : ℕ) : IsClosedMap fun x : R ↦ x ^ n := by - simpa [eval_X_pow] using (X ^ n).isClosedMap_eval + have := (X ^ n : R[X]).isClosedMap_eval + simpa [eval_X_pow] using this section Roots